# HG changeset patch # User wenzelm # Date 1331807876 -3600 # Node ID c0f776b661fab9edccd5259e90430a0d83fb4e59 # Parent a40be2f10ca90de461fa5915a642153a15212ce6 maintain Version.syntax within document state; clarified Outer_Syntax.empty vs. Outer_Syntax.init, which pulls in Isabelle_System symbol completions; diff -r a40be2f10ca9 -r c0f776b661fa src/Pure/Isar/outer_syntax.scala --- a/src/Pure/Isar/outer_syntax.scala Thu Mar 15 10:16:21 2012 +0100 +++ b/src/Pure/Isar/outer_syntax.scala Thu Mar 15 11:37:56 2012 +0100 @@ -35,13 +35,15 @@ } type Decl = (String, Option[(String, List[String])]) - def init(): Outer_Syntax = new Outer_Syntax() + + val empty: Outer_Syntax = new Outer_Syntax() + def init(): Outer_Syntax = new Outer_Syntax(completion = Completion.init()) } final class Outer_Syntax private( keywords: Map[String, String] = Map((";" -> Keyword.DIAG)), lexicon: Scan.Lexicon = Scan.Lexicon.empty, - val completion: Completion = Completion.init()) + val completion: Completion = Completion.empty) { def keyword_kind(name: String): Option[String] = keywords.get(name) diff -r a40be2f10ca9 -r c0f776b661fa src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Thu Mar 15 10:16:21 2012 +0100 +++ b/src/Pure/PIDE/document.scala Thu Mar 15 11:37:56 2012 +0100 @@ -212,12 +212,17 @@ { val init: Version = new Version() - def make(nodes: Nodes): Version = new Version(new_id(), nodes) + def make(syntax: Outer_Syntax, nodes: Nodes): Version = + new Version(new_id(), syntax, nodes) } final class Version private( val id: Version_ID = no_id, + val syntax: Outer_Syntax = Outer_Syntax.empty, val nodes: Nodes = Nodes.empty) + { + def is_init: Boolean = id == no_id + } /* changes of plain text, eventually resulting in document edits */ diff -r a40be2f10ca9 -r c0f776b661fa src/Pure/System/session.scala --- a/src/Pure/System/session.scala Thu Mar 15 10:16:21 2012 +0100 +++ b/src/Pure/System/session.scala Thu Mar 15 11:37:56 2012 +0100 @@ -86,7 +86,6 @@ //{{{ private case class Text_Edits( - syntax: Outer_Syntax, name: Document.Node.Name, previous: Future[Document.Version], text_edits: List[Document.Edit_Text], @@ -99,8 +98,9 @@ receive { case Stop => finished = true; reply(()) - case Text_Edits(syntax, name, previous, text_edits, version_result) => + case Text_Edits(name, previous, text_edits, version_result) => val prev = previous.get_finished + val syntax = if (prev.is_init) prover_syntax else prev.syntax val (doc_edits, version) = Thy_Syntax.text_edits(syntax, prev, text_edits) version_result.fulfill(version) sender ! Change_Node(name, doc_edits, prev, version) @@ -118,8 +118,11 @@ @volatile var verbose: Boolean = false - @volatile private var syntax = Outer_Syntax.init() - def current_syntax(): Outer_Syntax = syntax + @volatile private var prover_syntax = + Outer_Syntax.init() + + // FIXME avoid hardwired stuff!? + ("hence", Keyword.PRF_ASM_GOAL, "then have") + + ("thus", Keyword.PRF_ASM_GOAL, "then show") private val syslog = Volatile(Queue.empty[XML.Elem]) def current_syslog(): String = cat_lines(syslog().iterator.map(msg => XML.content(msg).mkString)) @@ -135,6 +138,7 @@ private val global_state = Volatile(Document.State.init) def current_state(): Document.State = global_state() + def recent_syntax(): Outer_Syntax = current_state().recent_stable.version.get_finished.syntax def snapshot(name: Document.Node.Name = Document.Node.Name.empty, pending_edits: List[Text.Edit] = Nil): Document.Snapshot = @@ -279,7 +283,6 @@ header: Document.Node_Header, edits: List[Document.Node.Edit[Text.Edit, Text.Perspective]]) //{{{ { - val syntax = current_syntax() val previous = global_state().history.tip.version prover.get.cancel_execution() @@ -288,7 +291,7 @@ val version = Future.promise[Document.Version] val change = global_state >>> (_.continue_history(previous, text_edits, version)) - change_parser ! Text_Edits(syntax, name, previous, text_edits, version) + change_parser ! Text_Edits(name, previous, text_edits, version) } //}}} @@ -398,19 +401,16 @@ System.err.println("cancel_scala " + id) // FIXME actually cancel JVM task case Isabelle_Markup.Ready if output.is_protocol => - // FIXME move to ML side (!?) - syntax += ("hence", Keyword.PRF_ASM_GOAL, "then have") - syntax += ("thus", Keyword.PRF_ASM_GOAL, "then show") phase = Session.Ready case Isabelle_Markup.Loaded_Theory(name) if output.is_protocol => thy_load.register_thy(name) case Isabelle_Markup.Command_Decl(name, kind) if output.is_protocol => - syntax += (name, kind) + prover_syntax += (name, kind) case Isabelle_Markup.Keyword_Decl(name) if output.is_protocol => - syntax += name + prover_syntax += name case _ => if (output.is_exit && phase == Session.Startup) phase = Session.Failed diff -r a40be2f10ca9 -r c0f776b661fa src/Pure/Thy/thy_syntax.scala --- a/src/Pure/Thy/thy_syntax.scala Thu Mar 15 10:16:21 2012 +0100 +++ b/src/Pure/Thy/thy_syntax.scala Thu Mar 15 11:37:56 2012 +0100 @@ -136,7 +136,7 @@ { val nodes = previous.nodes val (perspective, new_nodes) = update_perspective(nodes, name, text_perspective) - val version = Document.Version.make(new_nodes getOrElse nodes) + val version = Document.Version.make(previous.syntax, new_nodes getOrElse nodes) (perspective, version) } @@ -265,7 +265,7 @@ nodes = nodes1 } } - (doc_edits.toList, Document.Version.make(nodes)) + (doc_edits.toList, Document.Version.make(syntax, nodes)) } } } diff -r a40be2f10ca9 -r c0f776b661fa src/Tools/jEdit/src/isabelle_sidekick.scala --- a/src/Tools/jEdit/src/isabelle_sidekick.scala Thu Mar 15 10:16:21 2012 +0100 +++ b/src/Tools/jEdit/src/isabelle_sidekick.scala Thu Mar 15 11:37:56 2012 +0100 @@ -92,7 +92,7 @@ val start = buffer.getLineStartOffset(line) val text = buffer.getSegment(start, caret - start) - val completion = model.session.current_syntax().completion + val completion = model.session.recent_syntax().completion completion.complete(text) match { case None => null case Some((word, cs)) => @@ -116,7 +116,7 @@ def parser(data: SideKickParsedData, model: Document_Model) { - val syntax = model.session.current_syntax() + val syntax = model.session.recent_syntax() def make_tree(offset: Text.Offset, entry: Structure.Entry): List[DefaultMutableTreeNode] = entry match { diff -r a40be2f10ca9 -r c0f776b661fa src/Tools/jEdit/src/token_markup.scala --- a/src/Tools/jEdit/src/token_markup.scala Thu Mar 15 10:16:21 2012 +0100 +++ b/src/Tools/jEdit/src/token_markup.scala Thu Mar 15 11:37:56 2012 +0100 @@ -178,7 +178,7 @@ { val (styled_tokens, context1) = if (line_ctxt.isDefined && Isabelle.session.is_ready) { - val syntax = Isabelle.session.current_syntax() + val syntax = Isabelle.session.recent_syntax() val (tokens, ctxt1) = syntax.scan_context(line, line_ctxt.get) val styled_tokens = tokens.map(tok => (Isabelle_Rendering.token_markup(syntax, tok), tok))