--- a/Admin/components/components.sha1 Thu Oct 16 19:26:28 2014 +0200
+++ b/Admin/components/components.sha1 Sat Oct 18 22:50:35 2014 +0200
@@ -56,6 +56,7 @@
054c1300128f8abd0f46a3e92c756ccdb96ff2af jedit_build-20140405.tar.gz
4a963665537ea66c69de4d761846541ebdbf69f2 jedit_build-20140511.tar.gz
a9d637a30f6a87a3583f265da51e63e3619cff52 jedit_build-20140722.tar.gz
+f29391c53d85715f8454e1aaa304fbccc352928f jedit_build-20141018.tar.gz
0bd2bc2d9a491ba5fc8dd99df27c04f11a72e8fa jfreechart-1.0.14-1.tar.gz
8122526f1fc362ddae1a328bdbc2152853186fee jfreechart-1.0.14.tar.gz
c8a19a36adf6cefa779d85f22ded2f4654e68ea5 jortho-1.0-1.tar.gz
--- a/Admin/components/main Thu Oct 16 19:26:28 2014 +0200
+++ b/Admin/components/main Sat Oct 18 22:50:35 2014 +0200
@@ -5,7 +5,7 @@
exec_process-1.0.3
Haskabelle-2014
jdk-7u67
-jedit_build-20140722
+jedit_build-20141018
jfreechart-1.0.14-1
jortho-1.0-2
kodkodi-1.5.2
--- a/NEWS Thu Oct 16 19:26:28 2014 +0200
+++ b/NEWS Sat Oct 18 22:50:35 2014 +0200
@@ -17,6 +17,8 @@
*** Prover IDE -- Isabelle/Scala/jEdit ***
+* Improved folding mode "isabelle" based on Isar syntax.
+
* Support for BibTeX files: context menu, context-sensitive token
marker, SideKick parser.
--- a/src/Pure/Isar/outer_syntax.scala Thu Oct 16 19:26:28 2014 +0200
+++ b/src/Pure/Isar/outer_syntax.scala Sat Oct 18 22:50:35 2014 +0200
@@ -37,6 +37,21 @@
val empty: Outer_Syntax = new Outer_Syntax()
def init(): Outer_Syntax = new Outer_Syntax(completion = Completion.init())
+
+
+ /* line-oriented structure */
+
+ object Line_Structure
+ {
+ val init = Line_Structure()
+ }
+
+ sealed case class Line_Structure(
+ improper: Boolean = true,
+ command: Boolean = false,
+ depth: Int = 0,
+ span_depth: Int = 0,
+ after_span_depth: Int = 0)
}
final class Outer_Syntax private(
@@ -54,9 +69,25 @@
(if (files.isEmpty) "" else " (" + commas_quote(files) + ")")
}).toList.sorted.mkString("keywords\n ", " and\n ", "")
+
+ /* keyword kind */
+
def keyword_kind_files(name: String): Option[(String, List[String])] = keywords.get(name)
def keyword_kind(name: String): Option[String] = keyword_kind_files(name).map(_._1)
+ def is_command(name: String): Boolean =
+ keyword_kind(name) match {
+ case Some(kind) => kind != Keyword.MINOR
+ case None => false
+ }
+
+ def command_kind(token: Token, pred: String => Boolean): Boolean =
+ token.is_command && is_command(token.source) &&
+ pred(keyword_kind(token.source).get)
+
+
+ /* load commands */
+
def load_command(name: String): Option[List[String]] =
keywords.get(name) match {
case Some((Keyword.THY_LOAD, exts)) => Some(exts)
@@ -69,6 +100,9 @@
def load_commands_in(text: String): Boolean =
load_commands.exists({ case (cmd, _) => text.containsSlice(cmd) })
+
+ /* add keywords */
+
def + (name: String, kind: (String, List[String]), replace: Option[String]): Outer_Syntax =
{
val keywords1 = keywords + (name -> kind)
@@ -99,11 +133,8 @@
(Symbol.encode(name), replace)
}
- def is_command(name: String): Boolean =
- keyword_kind(name) match {
- case Some(kind) => kind != Keyword.MINOR
- case None => false
- }
+
+ /* document headings */
def heading_level(name: String): Option[Int] =
{
@@ -122,6 +153,37 @@
heading_level(command.name)
+ /* line-oriented structure */
+
+ def line_structure(tokens: List[Token], struct: Outer_Syntax.Line_Structure)
+ : Outer_Syntax.Line_Structure =
+ {
+ val improper1 = tokens.forall(_.is_improper)
+ val command1 = tokens.exists(_.is_command)
+
+ val depth1 =
+ if (tokens.exists(tok => command_kind(tok, Keyword.theory))) 0
+ else if (command1) struct.after_span_depth
+ else struct.span_depth
+
+ val (span_depth1, after_span_depth1) =
+ ((struct.span_depth, struct.after_span_depth) /: tokens) {
+ case ((x, y), tok) =>
+ if (tok.is_command) {
+ if (command_kind(tok, Keyword.theory_goal)) (2, 1)
+ else if (command_kind(tok, Keyword.theory)) (1, 0)
+ else if (command_kind(tok, Keyword.proof_goal) || tok.source == "{") (y + 2, y + 1)
+ else if (command_kind(tok, Keyword.qed) || tok.source == "}") (y + 1, y - 1)
+ else if (command_kind(tok, Keyword.qed_global)) (1, 0)
+ else (x, y)
+ }
+ else (x, y)
+ }
+
+ Outer_Syntax.Line_Structure(improper1, command1, depth1, span_depth1, after_span_depth1)
+ }
+
+
/* token language */
def scan(input: CharSequence): List[Token] =
@@ -134,7 +196,11 @@
}
}
- def scan_line(input: CharSequence, context: Scan.Line_Context): (List[Token], Scan.Line_Context) =
+ def scan_line(
+ input: CharSequence,
+ context: Scan.Line_Context,
+ structure: Outer_Syntax.Line_Structure)
+ : (List[Token], Scan.Line_Context, Outer_Syntax.Line_Structure) =
{
var in: Reader[Char] = new CharSequenceReader(input)
val toks = new mutable.ListBuffer[Token]
@@ -146,7 +212,8 @@
error("Unexpected failure of tokenizing input:\n" + rest.source.toString)
}
}
- (toks.toList, ctxt)
+ val tokens = toks.toList
+ (tokens, ctxt, line_structure(tokens, structure))
}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/patches/folding Sat Oct 18 22:50:35 2014 +0200
@@ -0,0 +1,47 @@
+diff -ru jEdit/org/gjt/sp/jedit/buffer/JEditBuffer.java jEdit-patched/org/gjt/sp/jedit/buffer/JEditBuffer.java
+--- jEdit/org/gjt/sp/jedit/buffer/JEditBuffer.java 2013-07-28 19:03:27.000000000 +0200
++++ jEdit-patched/org/gjt/sp/jedit/buffer/JEditBuffer.java 2014-10-18 21:35:15.946285279 +0200
+@@ -1945,29 +1945,23 @@
+ {
+ Segment seg = new Segment();
+ newFoldLevel = foldHandler.getFoldLevel(this,i,seg);
+- if(newFoldLevel != lineMgr.getFoldLevel(i))
++ if(Debug.FOLD_DEBUG)
++ Log.log(Log.DEBUG,this,i + " fold level changed");
++ changed = true;
++ // Update preceding fold levels if necessary
++ List<Integer> precedingFoldLevels =
++ foldHandler.getPrecedingFoldLevels(
++ this,i,seg,newFoldLevel);
++ if (precedingFoldLevels != null)
+ {
+- if(Debug.FOLD_DEBUG)
+- Log.log(Log.DEBUG,this,i + " fold level changed");
+- changed = true;
+- // Update preceding fold levels if necessary
+- if (i == firstInvalidFoldLevel)
++ int j = i;
++ for (Integer foldLevel: precedingFoldLevels)
+ {
+- List<Integer> precedingFoldLevels =
+- foldHandler.getPrecedingFoldLevels(
+- this,i,seg,newFoldLevel);
+- if (precedingFoldLevels != null)
+- {
+- int j = i;
+- for (Integer foldLevel: precedingFoldLevels)
+- {
+- j--;
+- lineMgr.setFoldLevel(j,foldLevel.intValue());
+- }
+- if (j < firstUpdatedFoldLevel)
+- firstUpdatedFoldLevel = j;
+- }
++ j--;
++ lineMgr.setFoldLevel(j,foldLevel.intValue());
+ }
++ if (j < firstUpdatedFoldLevel)
++ firstUpdatedFoldLevel = j;
+ }
+ lineMgr.setFoldLevel(i,newFoldLevel);
+ }
--- a/src/Tools/jEdit/src/Isabelle.props Thu Oct 16 19:26:28 2014 +0200
+++ b/src/Tools/jEdit/src/Isabelle.props Sat Oct 18 22:50:35 2014 +0200
@@ -79,7 +79,7 @@
mode.isabelle-root.folding=sidekick
mode.isabelle-root.sidekick.parser=isabelle-root
mode.isabelle.customSettings=true
-mode.isabelle.folding=sidekick
+mode.isabelle.folding=isabelle
mode.isabelle.sidekick.parser=isabelle
mode.isabelle.sidekick.showStatusWindow.label=true
mode.ml.sidekick.parser=isabelle
--- a/src/Tools/jEdit/src/bibtex_jedit.scala Thu Oct 16 19:26:28 2014 +0200
+++ b/src/Tools/jEdit/src/bibtex_jedit.scala Sat Oct 18 22:50:35 2014 +0200
@@ -153,8 +153,16 @@
private val context_rules = new ParserRuleSet("bibtex", "MAIN")
- private class Line_Context(context: Option[Bibtex.Line_Context])
- extends Token_Markup.Generic_Line_Context[Bibtex.Line_Context](context_rules, context)
+ private class Line_Context(val context: Option[Bibtex.Line_Context])
+ extends TokenMarker.LineContext(context_rules, null)
+ {
+ override def hashCode: Int = context.hashCode
+ override def equals(that: Any): Boolean =
+ that match {
+ case other: Line_Context => context == other.context
+ case _ => false
+ }
+ }
/* token marker */
--- a/src/Tools/jEdit/src/fold_handling.scala Thu Oct 16 19:26:28 2014 +0200
+++ b/src/Tools/jEdit/src/fold_handling.scala Sat Oct 18 22:50:35 2014 +0200
@@ -9,13 +9,47 @@
import isabelle._
-import org.gjt.sp.jedit.buffer.{JEditBuffer, FoldHandler}
+import javax.swing.text.Segment
-import javax.swing.text.Segment
+import scala.collection.convert.WrapAsJava
+
+import org.gjt.sp.jedit.buffer.{JEditBuffer, FoldHandler}
object Fold_Handling
{
+ /* input: dynamic line context */
+
+ class Fold_Handler extends FoldHandler("isabelle")
+ {
+ override def equals(other: Any): Boolean =
+ other match {
+ case that: Fold_Handler => true
+ case _ => false
+ }
+
+ override def getFoldLevel(buffer: JEditBuffer, line: Int, seg: Segment): Int =
+ Token_Markup.buffer_line_structure(buffer, line).depth max 0
+
+ override def getPrecedingFoldLevels(
+ buffer: JEditBuffer, line: Int, seg: Segment, level: Int): java.util.List[Integer] =
+ {
+ val struct = Token_Markup.buffer_line_structure(buffer, line)
+ val result =
+ if (line > 0 && struct.command)
+ Range.inclusive(line - 1, 0, -1).iterator.
+ map(Token_Markup.buffer_line_structure(buffer, _)).
+ takeWhile(_.improper).map(_ => struct.depth max 0).toList
+ else Nil
+
+ if (result.isEmpty) null
+ else WrapAsJava.seqAsJavaList(result.map(i => new Integer(i)))
+ }
+ }
+
+
+ /* output: static document rendering */
+
class Document_Fold_Handler(private val rendering: Rendering)
extends FoldHandler("isabelle-document")
{
@@ -30,8 +64,8 @@
def depth(i: Text.Offset): Int =
if (i < 0) 0
else {
- rendering.fold_depth(Text.Range(i, i + 1)).map(_.info) match {
- case d :: _ => d
+ rendering.fold_depth(Text.Range(i, i + 1)) match {
+ case Text.Info(_, d) :: _ => d
case _ => 0
}
}
--- a/src/Tools/jEdit/src/services.xml Thu Oct 16 19:26:28 2014 +0200
+++ b/src/Tools/jEdit/src/services.xml Sat Oct 18 22:50:35 2014 +0200
@@ -2,12 +2,15 @@
<!DOCTYPE SERVICES SYSTEM "services.dtd">
<SERVICES>
+ <SERVICE CLASS="org.gjt.sp.jedit.buffer.FoldHandler" NAME="isabelle">
+ new isabelle.jedit.Fold_Handling.Fold_Handler();
+ </SERVICE>
<SERVICE CLASS="org.gjt.sp.jedit.gui.DynamicContextMenuService" NAME="Spell_Checker">
new isabelle.jedit.Context_Menu();
</SERVICE>
- <SERVICE CLASS="org.gjt.sp.jedit.gui.DockingFrameworkProvider" NAME="PIDE">
- new isabelle.jedit.PIDE_Docking_Framework();
- </SERVICE>
+ <SERVICE CLASS="org.gjt.sp.jedit.gui.DockingFrameworkProvider" NAME="PIDE">
+ new isabelle.jedit.PIDE_Docking_Framework();
+ </SERVICE>
<SERVICE NAME="UTF-8-Isabelle" CLASS="org.gjt.sp.jedit.io.Encoding">
new isabelle.jedit.Isabelle_Encoding();
</SERVICE>
--- a/src/Tools/jEdit/src/token_markup.scala Thu Oct 16 19:26:28 2014 +0200
+++ b/src/Tools/jEdit/src/token_markup.scala Sat Oct 18 22:50:35 2014 +0200
@@ -15,8 +15,8 @@
import org.gjt.sp.util.SyntaxUtilities
import org.gjt.sp.jedit.{jEdit, Mode}
-import org.gjt.sp.jedit.syntax.{Token => JEditToken, TokenMarker, TokenHandler, ParserRuleSet,
- ModeProvider, XModeHandler, SyntaxStyle}
+import org.gjt.sp.jedit.syntax.{Token => JEditToken, TokenMarker, TokenHandler, DummyTokenHandler,
+ ParserRuleSet, ModeProvider, XModeHandler, SyntaxStyle}
import org.gjt.sp.jedit.textarea.{TextArea, Selection}
import org.gjt.sp.jedit.buffer.{JEditBuffer, LineManager}
@@ -175,32 +175,41 @@
/* line context */
- class Generic_Line_Context[C](rules: ParserRuleSet, val context: Option[C])
- extends TokenMarker.LineContext(rules, null)
+ private val context_rules = new ParserRuleSet("isabelle", "MAIN")
+
+ class Line_Context(
+ val context: Option[Scan.Line_Context],
+ val structure: Outer_Syntax.Line_Structure)
+ extends TokenMarker.LineContext(context_rules, null)
{
- override def hashCode: Int = context.hashCode
+ override def hashCode: Int = (context, structure).hashCode
override def equals(that: Any): Boolean =
that match {
- case other: Line_Context => context == other.context
+ case other: Line_Context => context == other.context && structure == other.structure
case _ => false
}
}
- def buffer_line_context[C](buffer: JEditBuffer, line: Int): Option[Generic_Line_Context[C]] =
+ def buffer_line_context(buffer: JEditBuffer, line: Int): Option[Line_Context] =
Untyped.get(buffer, "lineMgr") match {
case line_mgr: LineManager =>
- line_mgr.getLineContext(line) match {
- case ctxt: Generic_Line_Context[C] => Some(ctxt)
- case _ => None
+ def context =
+ line_mgr.getLineContext(line) match {
+ case c: Line_Context => Some(c)
+ case _ => None
+ }
+ context orElse {
+ buffer.markTokens(line, DummyTokenHandler.INSTANCE)
+ context
}
case _ => None
}
-
- private val context_rules = new ParserRuleSet("isabelle", "MAIN")
-
- private class Line_Context(context: Option[Scan.Line_Context])
- extends Generic_Line_Context[Scan.Line_Context](context_rules, context)
+ def buffer_line_structure(buffer: JEditBuffer, line: Int): Outer_Syntax.Line_Structure =
+ buffer_line_context(buffer, line) match {
+ case Some(c) => c.structure
+ case _ => Outer_Syntax.Line_Structure.init
+ }
/* token marker */
@@ -210,38 +219,31 @@
override def markTokens(context: TokenMarker.LineContext,
handler: TokenHandler, raw_line: Segment): TokenMarker.LineContext =
{
- val line_ctxt =
+ val (opt_ctxt, structure) =
context match {
- case c: Line_Context => c.context
- case _ => Some(Scan.Finished)
+ case c: Line_Context => (c.context, c.structure)
+ case _ => (Some(Scan.Finished), Outer_Syntax.Line_Structure.init)
}
val line = if (raw_line == null) new Segment else raw_line
val context1 =
{
- def no_context =
- {
- val styled_token = (JEditToken.NULL, line.subSequence(0, line.count).toString)
- (List(styled_token), new Line_Context(None))
- }
val (styled_tokens, context1) =
- if (mode == "isabelle-ml" || mode == "sml") {
- if (line_ctxt.isDefined) {
- val (tokens, ctxt1) = ML_Lex.tokenize_line(mode == "sml", line, line_ctxt.get)
+ (opt_ctxt, Isabelle.mode_syntax(mode)) match {
+ case (Some(ctxt), _) if mode == "isabelle-ml" || mode == "sml" =>
+ val (tokens, ctxt1) = ML_Lex.tokenize_line(mode == "sml", line, ctxt)
val styled_tokens = tokens.map(tok => (Rendering.ml_token_markup(tok), tok.source))
- (styled_tokens, new Line_Context(Some(ctxt1)))
- }
- else no_context
- }
- else {
- Isabelle.mode_syntax(mode) match {
- case Some(syntax) if syntax.has_tokens && line_ctxt.isDefined =>
- val (tokens, ctxt1) = syntax.scan_line(line, line_ctxt.get)
- val styled_tokens =
- tokens.map(tok => (Rendering.token_markup(syntax, tok), tok.source))
- (styled_tokens, new Line_Context(Some(ctxt1)))
- case _ => no_context
- }
+ (styled_tokens, new Line_Context(Some(ctxt1), structure))
+
+ case (Some(ctxt), Some(syntax)) if syntax.has_tokens =>
+ val (tokens, ctxt1, structure1) = syntax.scan_line(line, ctxt, structure)
+ val styled_tokens =
+ tokens.map(tok => (Rendering.token_markup(syntax, tok), tok.source))
+ (styled_tokens, new Line_Context(Some(ctxt1), structure1))
+
+ case _ =>
+ val styled_token = (JEditToken.NULL, line.subSequence(0, line.count).toString)
+ (List(styled_token), new Line_Context(None, structure))
}
val extended = extended_styles(line)
@@ -267,6 +269,7 @@
handler.handleToken(line, JEditToken.END, line.count, 0, context1)
context1
}
+
val context2 = context1.intern
handler.setLineContext(context2)
context2