# HG changeset patch # User wenzelm # Date 1344371117 -7200 # Node ID 73e6c22e2d949a283fe9f23bed47efb0a575884c # Parent 622251b2b0f1d04d3e323bf5d0b07885dabf0fed more structural parsing for minor modes; tuned signatures; diff -r 622251b2b0f1 -r 73e6c22e2d94 src/Pure/Isar/parse.scala --- a/src/Pure/Isar/parse.scala Tue Aug 07 21:38:24 2012 +0200 +++ b/src/Pure/Isar/parse.scala Tue Aug 07 22:25:17 2012 +0200 @@ -50,9 +50,11 @@ def atom(s: String, pred: Elem => Boolean): Parser[String] = token(s, pred) ^^ (_.content) + def command(name: String): Parser[String] = + atom("command " + quote(name), tok => tok.is_command && tok.source == name) + def keyword(name: String): Parser[String] = - atom(Token.Kind.KEYWORD.toString + " " + quote(name), - tok => tok.kind == Token.Kind.KEYWORD && tok.content == name) + atom("keyword " + quote(name), tok => tok.is_keyword && tok.source == name) def string: Parser[String] = atom("string", _.is_string) def nat: Parser[Int] = atom("natural number", _.is_nat) ^^ (s => Integer.parseInt(s)) diff -r 622251b2b0f1 -r 73e6c22e2d94 src/Pure/Isar/token.scala --- a/src/Pure/Isar/token.scala Tue Aug 07 21:38:24 2012 +0200 +++ b/src/Pure/Isar/token.scala Tue Aug 07 22:25:17 2012 +0200 @@ -67,7 +67,8 @@ sealed case class Token(val kind: Token.Kind.Value, val source: String) { def is_command: Boolean = kind == Token.Kind.COMMAND - def is_operator: Boolean = kind == Token.Kind.KEYWORD && !Symbol.is_ascii_identifier(source) + def is_keyword: Boolean = kind == Token.Kind.KEYWORD + def is_operator: Boolean = is_keyword && !Symbol.is_ascii_identifier(source) def is_delimited: Boolean = kind == Token.Kind.STRING || kind == Token.Kind.ALT_STRING || @@ -90,8 +91,8 @@ def is_proper: Boolean = !is_space && !is_comment def is_unparsed: Boolean = kind == Token.Kind.UNPARSED - def is_begin: Boolean = kind == Token.Kind.KEYWORD && source == "begin" - def is_end: Boolean = kind == Token.Kind.COMMAND && source == "end" + def is_begin: Boolean = is_keyword && source == "begin" + def is_end: Boolean = is_keyword && source == "end" def content: String = if (kind == Token.Kind.STRING) Scan.Lexicon.empty.quoted_content("\"", source) @@ -101,7 +102,7 @@ else source def text: (String, String) = - if (kind == Token.Kind.COMMAND && source == ";") ("terminator", "") + if (is_command && source == ";") ("terminator", "") else (kind.toString, source) } diff -r 622251b2b0f1 -r 73e6c22e2d94 src/Pure/PIDE/command.scala --- a/src/Pure/PIDE/command.scala Tue Aug 07 21:38:24 2012 +0200 +++ b/src/Pure/PIDE/command.scala Tue Aug 07 22:25:17 2012 +0200 @@ -133,7 +133,7 @@ def is_command: Boolean = !is_ignored && !is_malformed def name: String = - span.find(_.is_command) match { case Some(tok) => tok.content case _ => "" } + span.find(_.is_command) match { case Some(tok) => tok.source case _ => "" } override def toString = id + "/" + (if (is_command) name else if (is_ignored) "IGNORED" else "MALFORMED") diff -r 622251b2b0f1 -r 73e6c22e2d94 src/Pure/System/build.scala --- a/src/Pure/System/build.scala Tue Aug 07 21:38:24 2012 +0200 +++ b/src/Pure/System/build.scala Tue Aug 07 22:25:17 2012 +0200 @@ -172,7 +172,7 @@ lazy val root_syntax = Outer_Syntax.init() + "!" + "(" + ")" + "+" + "," + "=" + "[" + "]" + - SESSION + IN + DESCRIPTION + OPTIONS + THEORIES + FILES + (SESSION, Keyword.THY_DECL) + IN + DESCRIPTION + OPTIONS + THEORIES + FILES private object Parser extends Parse.Parser { @@ -188,7 +188,7 @@ keyword(THEORIES) ~! ((options | success(Nil)) ~ rep1(theory_name)) ^^ { case _ ~ (x ~ y) => (x, y) } - ((keyword(SESSION) ~! session_name) ^^ { case _ ~ x => x }) ~ + ((command(SESSION) ~! session_name) ^^ { case _ ~ x => x }) ~ (keyword("!") ^^^ true | success(false)) ~ (keyword("(") ~! (rep1(name) <~ keyword(")")) ^^ { case _ ~ x => x } | success(Nil)) ~ (opt(keyword(IN) ~! path ^^ { case _ ~ x => x })) ~ diff -r 622251b2b0f1 -r 73e6c22e2d94 src/Pure/System/options.scala --- a/src/Pure/System/options.scala Tue Aug 07 21:38:24 2012 +0200 +++ b/src/Pure/System/options.scala Tue Aug 07 22:25:17 2012 +0200 @@ -33,7 +33,9 @@ private val DECLARE = "declare" private val DEFINE = "define" - lazy val options_syntax = Outer_Syntax.init() + ":" + "=" + "--" + DECLARE + DEFINE + lazy val options_syntax = + Outer_Syntax.init() + ":" + "=" + "--" + + (DECLARE, Keyword.THY_DECL) + (DEFINE, Keyword.PRF_DECL) private object Parser extends Parse.Parser { @@ -47,10 +49,10 @@ { case s ~ n => if (s.isDefined) "-" + n else n } | atom("option value", tok => tok.is_name || tok.is_float) - keyword(DECLARE) ~! (option_name ~ keyword(":") ~ option_type ~ + command(DECLARE) ~! (option_name ~ keyword(":") ~ option_type ~ keyword("=") ~ option_value ~ (keyword("--") ~! text ^^ { case _ ~ x => x } | success(""))) ^^ { case _ ~ (a ~ _ ~ b ~ _ ~ c ~ d) => (options: Options) => options.declare(a, b, c, d) } | - keyword(DEFINE) ~! (option_name ~ keyword("=") ~ option_value) ^^ + command(DEFINE) ~! (option_name ~ keyword("=") ~ option_value) ^^ { case _ ~ (a ~ _ ~ b) => (options: Options) => options.define(a, b) } } diff -r 622251b2b0f1 -r 73e6c22e2d94 src/Pure/Thy/thy_syntax.scala --- a/src/Pure/Thy/thy_syntax.scala Tue Aug 07 21:38:24 2012 +0200 +++ b/src/Pure/Thy/thy_syntax.scala Tue Aug 07 22:25:17 2012 +0200 @@ -33,7 +33,7 @@ def buffer(): mutable.ListBuffer[Entry] = new mutable.ListBuffer[Entry] var stack: List[(Int, String, mutable.ListBuffer[Entry])] = - List((0, "theory " + node_name.theory, buffer())) + List((0, node_name.theory, buffer())) @tailrec def close(level: Int => Boolean) { diff -r 622251b2b0f1 -r 73e6c22e2d94 src/Tools/jEdit/src/Isabelle.props --- a/src/Tools/jEdit/src/Isabelle.props Tue Aug 07 21:38:24 2012 +0200 +++ b/src/Tools/jEdit/src/Isabelle.props Tue Aug 07 22:25:17 2012 +0200 @@ -67,15 +67,16 @@ isabelle-syslog.title=Syslog #SideKick -mode.isabelle.sidekick.showStatusWindow.label=true -sidekick.parser.isabelle.label=Isabelle -mode.isabelle.sidekick.parser=isabelle +mode.isabelle-options.folding=sidekick mode.isabelle-options.sidekick.parser=isabelle-options +mode.isabelle-root.folding=sidekick mode.isabelle-root.sidekick.parser=isabelle-root -mode.ml.sidekick.parser=isabelle - mode.isabelle.customSettings=true mode.isabelle.folding=sidekick +mode.isabelle.sidekick.parser=isabelle +mode.isabelle.sidekick.showStatusWindow.label=true +mode.ml.sidekick.parser=isabelle +sidekick.parser.isabelle.label=Isabelle #Hyperlinks mode.isabelle.hyperlink.source=isabelle diff -r 622251b2b0f1 -r 73e6c22e2d94 src/Tools/jEdit/src/isabelle_sidekick.scala --- a/src/Tools/jEdit/src/isabelle_sidekick.scala Tue Aug 07 21:38:24 2012 +0200 +++ b/src/Tools/jEdit/src/isabelle_sidekick.scala Tue Aug 07 22:25:17 2012 +0200 @@ -132,8 +132,11 @@ } -class Isabelle_Sidekick_Default - extends Isabelle_Sidekick("isabelle", Isabelle.session.get_recent_syntax) +class Isabelle_Sidekick_Structure( + name: String, + get_syntax: => Option[Outer_Syntax], + node_name: Buffer => Option[Document.Node.Name]) + extends Isabelle_Sidekick(name, get_syntax) { import Thy_Syntax.Structure @@ -160,10 +163,10 @@ case _ => Nil } - Isabelle.buffer_node_name(buffer) match { - case Some(node_name) => + node_name(buffer) match { + case Some(name) => val text = Isabelle.buffer_text(buffer) - val structure = Structure.parse(syntax, node_name, text) + val structure = Structure.parse(syntax, name, text) make_tree(0, structure) foreach (node => data.root.add(node)) true case None => false @@ -172,12 +175,16 @@ } -class Isabelle_Sidekick_Options - extends Isabelle_Sidekick("isabelle-options", Some(Options.options_syntax)) +class Isabelle_Sidekick_Default extends Isabelle_Sidekick_Structure( + "isabelle", Isabelle.session.get_recent_syntax, Isabelle.buffer_node_name) -class Isabelle_Sidekick_Root - extends Isabelle_Sidekick("isabelle-root", Some(Build.root_syntax)) +class Isabelle_Sidekick_Options extends Isabelle_Sidekick_Structure( + "isabelle-options", Some(Options.options_syntax), Isabelle.buffer_node_dummy) + + +class Isabelle_Sidekick_Root extends Isabelle_Sidekick_Structure( + "isabelle-root", Some(Build.root_syntax), Isabelle.buffer_node_dummy) class Isabelle_Sidekick_Raw diff -r 622251b2b0f1 -r 73e6c22e2d94 src/Tools/jEdit/src/plugin.scala --- a/src/Tools/jEdit/src/plugin.scala Tue Aug 07 21:38:24 2012 +0200 +++ b/src/Tools/jEdit/src/plugin.scala Tue Aug 07 22:25:17 2012 +0200 @@ -147,6 +147,15 @@ def buffer_name(buffer: Buffer): String = buffer.getSymlinkPath + def buffer_node_dummy(buffer: Buffer): Option[Document.Node.Name] = + Some(Document.Node.Name(buffer_name(buffer), buffer.getDirectory, buffer.getName)) + + def buffer_node_name(buffer: Buffer): Option[Document.Node.Name] = + { + val name = buffer_name(buffer) + Thy_Header.thy_name(name).map(theory => Document.Node.Name(name, buffer.getDirectory, theory)) + } + /* main jEdit components */ @@ -193,12 +202,6 @@ } } - def buffer_node_name(buffer: Buffer): Option[Document.Node.Name] = - { - val name = buffer_name(buffer) - Thy_Header.thy_name(name).map(theory => Document.Node.Name(name, buffer.getDirectory, theory)) - } - def init_model(buffer: Buffer) { swing_buffer_lock(buffer) {