Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
P
ProofScriptParser
Project overview
Project overview
Details
Activity
Releases
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Issues
24
Issues
24
List
Boards
Labels
Service Desk
Milestones
Merge Requests
4
Merge Requests
4
CI / CD
CI / CD
Pipelines
Jobs
Schedules
Operations
Operations
Incidents
Environments
Analytics
Analytics
CI / CD
Repository
Value Stream
Wiki
Wiki
Snippets
Snippets
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Create a new issue
Jobs
Commits
Issue Boards
Open sidebar
sarah.grebing
ProofScriptParser
Commits
ed44f370
Commit
ed44f370
authored
Jun 05, 2017
by
Alexander Weigl
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
better issue support
parent
0abbf1e7
Pipeline
#10942
failed with stage
in 2 minutes and 15 seconds
Changes
7
Pipelines
1
Hide whitespace changes
Inline
Side-by-side
Showing
7 changed files
with
297 additions
and
15 deletions
+297
-15
pom.xml
pom.xml
+36
-0
src/main/java/edu/kit/formal/gui/ProofScriptDebugger.java
src/main/java/edu/kit/formal/gui/ProofScriptDebugger.java
+4
-0
src/main/java/edu/kit/formal/gui/controls/ScriptArea.java
src/main/java/edu/kit/formal/gui/controls/ScriptArea.java
+53
-9
src/main/java/edu/kit/formal/proofscriptparser/lint/LintProblem.java
...va/edu/kit/formal/proofscriptparser/lint/LintProblem.java
+133
-4
src/main/resources/edu/kit/formal/proofscriptparser/lint/lint-issues-en.xml
.../edu/kit/formal/proofscriptparser/lint/lint-issues-en.xml
+6
-2
src/main/resources/proofscriptdebugger.css
src/main/resources/proofscriptdebugger.css
+27
-0
src/test/java/edu/kit/formal/proofscriptparser/lint/LintProblemTest.java
...du/kit/formal/proofscriptparser/lint/LintProblemTest.java
+38
-0
No files found.
pom.xml
View file @
ed44f370
...
...
@@ -123,6 +123,36 @@
<mainClass>
ProofScriptDebugger.Main
</mainClass>
</configuration>
</plugin>
<plugin>
<groupId>
org.apache.maven.plugins
</groupId>
<artifactId>
maven-shade-plugin
</artifactId>
<version>
2.4.3
</version>
<configuration>
<!-- put your configurations here -->
</configuration>
<executions>
<execution>
<phase>
package
</phase>
<goals>
<goal>
shade
</goal>
</goals>
<configuration>
<minimizeJar>
true
</minimizeJar>
<finalName>
${project.name}-${project.version}-exe
</finalName>
<transformers>
<transformer
implementation=
"org.apache.maven.plugins.shade.resource.ManifestResourceTransformer"
>
<mainClass>
edu.kit.formal.gui.ProofScriptDebugger
</mainClass>
</transformer>
</transformers>
</configuration>
</execution>
</executions>
</plugin>
</plugins>
</build>
...
...
@@ -247,6 +277,12 @@
<version>
2.6
</version>
</dependency>
<dependency>
<groupId>
com.github.spullara.mustache.java
</groupId>
<artifactId>
compiler
</artifactId>
<version>
0.9.2
</version>
</dependency>
</dependencies>
...
...
src/main/java/edu/kit/formal/gui/ProofScriptDebugger.java
View file @
ed44f370
...
...
@@ -12,6 +12,7 @@ import javafx.application.Application;
import
javafx.fxml.FXMLLoader
;
import
javafx.scene.Parent
;
import
javafx.scene.Scene
;
import
javafx.scene.SceneBuilder
;
import
javafx.stage.Stage
;
import
java.io.IOException
;
...
...
@@ -41,6 +42,9 @@ public class ProofScriptDebugger extends Application {
Parent
root
=
fxmlLoader
.
load
();
//DebuggerMainWindowController controller = fxmlLoader.<DebuggerMainWindowController>getController();
Scene
scene
=
new
Scene
(
root
);
scene
.
getStylesheets
().
addAll
(
"/proofscriptdebugger.css"
);
primaryStage
.
setTitle
(
NAME
+
" ("
+
VERSION
+
") with KeY:"
+
KEY_VERSION
);
primaryStage
.
setScene
(
scene
);
primaryStage
.
show
();
...
...
src/main/java/edu/kit/formal/gui/controls/ScriptArea.java
View file @
ed44f370
...
...
@@ -6,17 +6,21 @@ import edu.kit.formal.proofscriptparser.Facade;
import
edu.kit.formal.proofscriptparser.ScriptLanguageLexer
;
import
edu.kit.formal.proofscriptparser.lint.LintProblem
;
import
edu.kit.formal.proofscriptparser.lint.LinterStrategy
;
import
javafx.beans.property.ListProperty
;
import
javafx.beans.property.SimpleListProperty
;
import
javafx.beans.property.SimpleObjectProperty
;
import
javafx.collections.FXCollections
;
import
javafx.collections.ObservableList
;
import
javafx.collections.ObservableSet
;
import
javafx.geometry.Insets
;
import
javafx.geometry.Point2D
;
import
javafx.geometry.Pos
;
import
javafx.scene.Node
;
import
javafx.scene.control.Label
;
import
javafx.scene.layout.Background
;
import
javafx.scene.layout.BackgroundFill
;
import
javafx.scene.layout.HBox
;
import
javafx.scene.layout.VBox
;
import
javafx.scene.paint.Color
;
import
javafx.scene.paint.Paint
;
import
javafx.scene.text.Font
;
...
...
@@ -24,12 +28,12 @@ import javafx.scene.text.FontPosture;
import
org.antlr.v4.runtime.CharStreams
;
import
org.antlr.v4.runtime.Token
;
import
org.fxmisc.richtext.CodeArea
;
import
org.fxmisc.richtext.MouseOverTextEvent
;
import
org.reactfx.collection.LiveList
;
import
org.reactfx.value.Val
;
import
java.
util.ArrayList
;
import
java.
time.Duration
;
import
java.util.Collections
;
import
java.util.List
;
import
java.util.function.IntFunction
;
/**
...
...
@@ -39,6 +43,8 @@ public class ScriptArea extends CodeArea {
private
ObservableSet
<
Integer
>
markedLines
=
FXCollections
.
observableSet
();
private
GutterFactory
gutter
;
private
ANTLR4LexerHighlighter
highlighter
;
private
ListProperty
<
LintProblem
>
problems
=
new
SimpleListProperty
<>(
FXCollections
.
observableArrayList
());
public
ScriptArea
()
{
init
();
...
...
@@ -68,6 +74,42 @@ public class ScriptArea extends CodeArea {
return Optional.empty();
}
}).subscribe(s -> setStyleSpans(0, s));*/
installPopup
();
}
private
void
installPopup
()
{
javafx
.
stage
.
Popup
popup
=
new
javafx
.
stage
.
Popup
();
setMouseOverTextDelay
(
Duration
.
ofSeconds
(
1
));
addEventHandler
(
MouseOverTextEvent
.
MOUSE_OVER_TEXT_BEGIN
,
e
->
{
int
chIdx
=
e
.
getCharacterIndex
();
popup
.
getContent
().
setAll
(
createPopupInformation
(
chIdx
)
);
Point2D
pos
=
e
.
getScreenPosition
();
popup
.
show
(
this
,
pos
.
getX
(),
pos
.
getY
()
+
10
);
});
addEventHandler
(
MouseOverTextEvent
.
MOUSE_OVER_TEXT_END
,
e
->
{
popup
.
hide
();
});
}
private
Node
createPopupInformation
(
int
chIdx
)
{
VBox
box
=
new
VBox
();
box
.
getStyleClass
().
add
(
"problem-popup"
);
for
(
LintProblem
p
:
problems
)
{
if
(
p
.
includeTextPosition
(
chIdx
))
{
Label
lbl
=
new
Label
(
p
.
getMessage
());
lbl
.
getStyleClass
().
addAll
(
"problem-popup-label"
,
"problem-popup-label-"
+
p
.
getIssue
().
getRulename
(),
"problem-popup-label-"
+
p
.
getIssue
().
getSeverity
());
box
.
getChildren
().
add
(
lbl
);
}
}
return
box
;
}
public
ObservableSet
<
Integer
>
getMarkedLines
()
{
...
...
@@ -80,13 +122,16 @@ public class ScriptArea extends CodeArea {
private
void
highlightProblems
()
{
LinterStrategy
ls
=
LinterStrategy
.
getDefaultLinter
();
List
<
LintProblem
>
pl
=
ls
.
check
(
Facade
.
getAST
(
CharStreams
.
fromString
(
getText
())));
for
(
LintProblem
p
:
pl
)
{
for
(
Token
tok
:
p
.
getMarkTokens
())
{
setStyle
(
tok
.
getStartIndex
(),
tok
.
getStopIndex
()+
1
,
Collections
.
singleton
(
"problem"
));
try
{
problems
.
setAll
(
ls
.
check
(
Facade
.
getAST
(
CharStreams
.
fromString
(
getText
()))));
for
(
LintProblem
p
:
problems
)
{
for
(
Token
tok
:
p
.
getMarkTokens
())
{
setStyle
(
tok
.
getStartIndex
(),
tok
.
getStopIndex
()
+
1
,
Collections
.
singleton
(
"problem"
));
}
}
}
catch
(
Exception
e
)
{
//catch parsing exceptions
}
}
...
...
@@ -106,7 +151,6 @@ public class ScriptArea extends CodeArea {
}
}
public
class
GutterFactory
implements
IntFunction
<
Node
>
{
private
Insets
defaultInsets
=
new
Insets
(
0.0
,
5.0
,
0.0
,
5.0
);
private
Paint
defaultTextFill
=
Color
.
web
(
"#666"
);
...
...
src/main/java/edu/kit/formal/proofscriptparser/lint/LintProblem.java
View file @
ed44f370
package
edu.kit.formal.proofscriptparser.lint
;
import
com.github.mustachejava.DefaultMustacheFactory
;
import
com.github.mustachejava.Mustache
;
import
com.github.mustachejava.reflect.ReflectionObjectHandler
;
import
edu.kit.formal.proofscriptparser.ast.ASTNode
;
import
lombok.Data
;
import
lombok.Getter
;
...
...
@@ -7,9 +10,10 @@ import lombok.RequiredArgsConstructor;
import
org.antlr.v4.runtime.ParserRuleContext
;
import
org.antlr.v4.runtime.Token
;
import
java.util.ArrayList
;
import
java.util.Arrays
;
import
java.util.List
;
import
java.io.StringReader
;
import
java.io.StringWriter
;
import
java.lang.reflect.Array
;
import
java.util.*
;
/**
* @author Alexander Weigl
...
...
@@ -20,10 +24,40 @@ import java.util.List;
public
class
LintProblem
{
@Getter
private
final
Issue
issue
;
private
final
Mustache
template
;
@Getter
private
List
<
Token
>
markTokens
=
new
ArrayList
<>();
private
static
DefaultMustacheFactory
mf
=
new
DefaultMustacheFactory
();
static
{
ReflectionObjectHandler
oh
=
new
ReflectionObjectHandler
()
{
@Override
public
Object
coerce
(
final
Object
object
)
{
if
(
object
!=
null
&&
object
.
getClass
().
isArray
())
{
return
new
ArrayMap
(
object
);
}
if
(
object
!=
null
&&
List
.
class
.
isAssignableFrom
(
object
.
getClass
()))
{
return
new
ListMap
((
List
)
object
);
}
return
super
.
coerce
(
object
);
}
};
mf
.
setObjectHandler
(
oh
);
}
public
LintProblem
(
Issue
issue
)
{
this
.
issue
=
issue
;
template
=
mf
.
compile
(
new
StringReader
(
issue
.
getValue
()),
issue
.
getRulename
());
}
public
Token
[]
toks
()
{
Token
[]
tokens
=
(
Token
[])
markTokens
.
toArray
(
new
Token
[
markTokens
.
size
()]);
return
tokens
;
}
public
Token
getFirstToken
()
{
if
(
markTokens
.
size
()
==
0
)
return
null
;
...
...
@@ -41,8 +75,11 @@ public class LintProblem {
return
lp
.
tokens
(
markTokens
);
}
public
String
getMessage
()
{
return
String
.
format
(
getIssue
().
getValue
(),
markTokens
.
toArray
());
StringWriter
sw
=
new
StringWriter
();
template
.
execute
(
sw
,
this
);
return
sw
.
toString
();
}
public
static
<
T
extends
ParserRuleContext
>
...
...
@@ -63,4 +100,96 @@ public class LintProblem {
getMarkTokens
().
addAll
(
Arrays
.
asList
(
toks
));
return
this
;
}
public
boolean
includeTextPosition
(
int
chIdx
)
{
//weigl: a little more relaxer that have to. Think on one length tokens.
return
markTokens
.
stream
().
anyMatch
(
tok
->
tok
.
getStartIndex
()
-
2
<=
chIdx
&&
chIdx
-
2
<=
tok
.
getStopIndex
());
}
}
class
ListMap
<
V
>
extends
AbstractMap
<
Integer
,
V
>
implements
Iterable
<
V
>
{
private
final
List
<
V
>
list
;
public
ListMap
(
List
<
V
>
list
)
{
this
.
list
=
list
;
}
@Override
public
V
get
(
Object
key
)
{
try
{
Integer
i
=
(
Integer
)
key
;
return
list
.
get
(
i
);
}
catch
(
ClassCastException
e
)
{
return
null
;
}
}
@Override
public
Set
<
Entry
<
Integer
,
V
>>
entrySet
()
{
throw
new
UnsupportedOperationException
();
}
@Override
public
Iterator
<
V
>
iterator
()
{
return
list
.
iterator
();
}
}
class
ArrayMap
extends
AbstractMap
<
Object
,
Object
>
implements
Iterable
<
Object
>
{
private
final
Object
object
;
public
ArrayMap
(
Object
object
)
{
this
.
object
=
object
;
}
@Override
public
Object
get
(
Object
key
)
{
try
{
int
index
=
Integer
.
parseInt
(
key
.
toString
());
return
Array
.
get
(
object
,
index
);
}
catch
(
NumberFormatException
nfe
)
{
return
null
;
}
}
@Override
public
boolean
containsKey
(
Object
key
)
{
return
get
(
key
)
!=
null
;
}
@Override
public
Set
<
Entry
<
Object
,
Object
>>
entrySet
()
{
throw
new
UnsupportedOperationException
();
}
/**
* Returns an iterator over a set of elements of type T.
*
* @return an Iterator.
*/
@Override
public
Iterator
<
Object
>
iterator
()
{
return
new
Iterator
<
Object
>()
{
int
index
=
0
;
int
length
=
Array
.
getLength
(
object
);
@Override
public
boolean
hasNext
()
{
return
index
<
length
;
}
@Override
public
Object
next
()
{
return
Array
.
get
(
object
,
index
++);
}
@Override
public
void
remove
()
{
throw
new
UnsupportedOperationException
();
}
};
}
}
src/main/resources/edu/kit/formal/proofscriptparser/lint/lint-issues-en.xml
View file @
ed44f370
...
...
@@ -2,10 +2,12 @@
<issue
id=
"0"
severity=
"info"
rulename=
"empty_blocks"
>
Empty blocks are useless!
</issue>
<issue
id=
"1"
severity=
"error"
rulename=
"equal_script_names"
>
The identifier of scripts need to be unique.
%0$s clashes with %1$s
.
{{markTokens.0.text}} clashes with {{markTokens.0.text}}
.
</issue>
<issue
id=
"2"
severity=
"error"
rulename=
"negated_match_with_using"
>
</issue>
...
...
@@ -13,7 +15,9 @@
<issue
id=
"3"
severity=
"warn"
rulename=
"succ_same_block"
>
Successive blocks have no effect!
</issue>
<issue
id=
"4"
severity=
"warn"
rulename=
"FOREACH_AFTER_THEONLY"
/>
<issue
id=
"4"
severity=
"warn"
rulename=
"FOREACH_AFTER_THEONLY"
>
{{firstToken.text}}
</issue>
<issue
id=
"5"
severity=
"warn"
rulename=
"THEONLY_AFTER_FOREACH"
/>
<issue
id=
"7"
severity=
"warn"
rulename=
"REDECLARE_VARIABLE"
>
...
...
src/main/resources/proofscriptdebugger.css
0 → 100644
View file @
ed44f370
.problem-popup
{
-fx-background-color
:
black
;
-fx-text-fill
:
white
;
-fx-padding
:
4px
;
-fx-border-radius
:
10
10
10
10
;
-fx-background-radius
:
10
10
10
10
;
-fx-text-alignment
:
center
;
-fx-wrap-text
:
true
;
-fx-spacing
:
5
;
-fx-fill-width
:
true
;
}
.problem-popup-label
{
-fx-wrap-text
:
true
;
}
.problem-popup-label-error
{
-fx-text-fill
:
firebrick
;
}
.problem-popup-label-warn
,
.problem-popup-label-warning
{
-fx-text-fill
:
darkorange
;
}
.problem-popup-label-info
{
-fx-text-fill
:
cornflowerblue
;
}
\ No newline at end of file
src/test/java/edu/kit/formal/proofscriptparser/lint/LintProblemTest.java
0 → 100644
View file @
ed44f370
package
edu.kit.formal.proofscriptparser.lint
;
import
org.antlr.v4.runtime.CommonToken
;
import
org.junit.Assert
;
import
org.junit.Before
;
import
org.junit.Test
;
/**
* @author Alexander Weigl
* @version 1 (04.06.17)
*/
public
class
LintProblemTest
{
Issue
issue
;
LintProblem
lp
;
@Before
public
void
setup
()
{
issue
=
new
Issue
();
issue
.
setId
(
2
);
issue
.
setRulename
(
"test"
);
issue
.
setValue
(
//"{{#toks}}{{text}}{{/toks}}" +
""
+
"{{toks.0.text}}"
+
""
);
lp
=
new
LintProblem
(
issue
);
lp
.
tokens
(
new
CommonToken
(
1
,
"test"
),
new
CommonToken
(
1
,
"abc"
)
);
}
@Test
public
void
getMessage
()
throws
Exception
{
Assert
.
assertEquals
(
"test"
,
lp
.
getMessage
());
}
}
\ No newline at end of file
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment