# HG changeset patch # User wenzelm # Date 1413665435 -7200 # Node ID ad09a4635e26eb1f3d208371d27bcdf9e0bf6d8d # Parent 68f8d22a68676bd98010b374a1fc87f375eb2c44# Parent 92f935f34b283ab38897feefb2b7ec4e21348864 merged diff -r 68f8d22a6867 -r ad09a4635e26 Admin/components/components.sha1 --- 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 diff -r 68f8d22a6867 -r ad09a4635e26 Admin/components/main --- 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 diff -r 68f8d22a6867 -r ad09a4635e26 NEWS --- 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. diff -r 68f8d22a6867 -r ad09a4635e26 src/Pure/Isar/outer_syntax.scala --- 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)) } diff -r 68f8d22a6867 -r ad09a4635e26 src/Tools/jEdit/patches/folding --- /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 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 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); + } diff -r 68f8d22a6867 -r ad09a4635e26 src/Tools/jEdit/src/Isabelle.props --- 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 diff -r 68f8d22a6867 -r ad09a4635e26 src/Tools/jEdit/src/bibtex_jedit.scala --- 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 */ diff -r 68f8d22a6867 -r ad09a4635e26 src/Tools/jEdit/src/fold_handling.scala --- 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 } } diff -r 68f8d22a6867 -r ad09a4635e26 src/Tools/jEdit/src/services.xml --- 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 @@ + + new isabelle.jedit.Fold_Handling.Fold_Handler(); + new isabelle.jedit.Context_Menu(); - - new isabelle.jedit.PIDE_Docking_Framework(); - + + new isabelle.jedit.PIDE_Docking_Framework(); + new isabelle.jedit.Isabelle_Encoding(); diff -r 68f8d22a6867 -r ad09a4635e26 src/Tools/jEdit/src/token_markup.scala --- 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