--- 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))
--- 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)
}
--- 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")
--- 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 })) ~
--- 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) }
}
--- 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)
{
--- 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
--- 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
--- 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) {