1.1 --- a/src/Pure/Isar/outer_syntax.scala	Thu Mar 15 10:16:21 2012 +0100
     1.2 +++ b/src/Pure/Isar/outer_syntax.scala	Thu Mar 15 11:37:56 2012 +0100
     1.3 @@ -35,13 +35,15 @@
     1.4    }
     1.5  
     1.6    type Decl = (String, Option[(String, List[String])])
     1.7 -  def init(): Outer_Syntax = new Outer_Syntax()
     1.8 +
     1.9 +  val empty: Outer_Syntax = new Outer_Syntax()
    1.10 +  def init(): Outer_Syntax = new Outer_Syntax(completion = Completion.init())
    1.11  }
    1.12  
    1.13  final class Outer_Syntax private(
    1.14    keywords: Map[String, String] = Map((";" -> Keyword.DIAG)),
    1.15    lexicon: Scan.Lexicon = Scan.Lexicon.empty,
    1.16 -  val completion: Completion = Completion.init())
    1.17 +  val completion: Completion = Completion.empty)
    1.18  {
    1.19    def keyword_kind(name: String): Option[String] = keywords.get(name)
    1.20  

     2.1 --- a/src/Pure/PIDE/document.scala	Thu Mar 15 10:16:21 2012 +0100
     2.2 +++ b/src/Pure/PIDE/document.scala	Thu Mar 15 11:37:56 2012 +0100
     2.3 @@ -212,12 +212,17 @@
     2.4    {
     2.5      val init: Version = new Version()
     2.6  
     2.7 -    def make(nodes: Nodes): Version = new Version(new_id(), nodes)
     2.8 +    def make(syntax: Outer_Syntax, nodes: Nodes): Version =
     2.9 +      new Version(new_id(), syntax, nodes)
    2.10    }
    2.11  
    2.12    final class Version private(
    2.13      val id: Version_ID = no_id,
    2.14 +    val syntax: Outer_Syntax = Outer_Syntax.empty,
    2.15      val nodes: Nodes = Nodes.empty)
    2.16 +  {
    2.17 +    def is_init: Boolean = id == no_id
    2.18 +  }
    2.19  
    2.20  
    2.21    /* changes of plain text, eventually resulting in document edits */

     3.1 --- a/src/Pure/System/session.scala	Thu Mar 15 10:16:21 2012 +0100
     3.2 +++ b/src/Pure/System/session.scala	Thu Mar 15 11:37:56 2012 +0100
     3.3 @@ -86,7 +86,6 @@
     3.4  
     3.5    //{{{
     3.6    private case class Text_Edits(
     3.7 -    syntax: Outer_Syntax,
     3.8      name: Document.Node.Name,
     3.9      previous: Future[Document.Version],
    3.10      text_edits: List[Document.Edit_Text],
    3.11 @@ -99,8 +98,9 @@
    3.12        receive {
    3.13          case Stop => finished = true; reply(())
    3.14  
    3.15 -        case Text_Edits(syntax, name, previous, text_edits, version_result) =>
    3.16 +        case Text_Edits(name, previous, text_edits, version_result) =>
    3.17            val prev = previous.get_finished
    3.18 +          val syntax = if (prev.is_init) prover_syntax else prev.syntax
    3.19            val (doc_edits, version) = Thy_Syntax.text_edits(syntax, prev, text_edits)
    3.20            version_result.fulfill(version)
    3.21            sender ! Change_Node(name, doc_edits, prev, version)
    3.22 @@ -118,8 +118,11 @@
    3.23  
    3.24    @volatile var verbose: Boolean = false
    3.25  
    3.26 -  @volatile private var syntax = Outer_Syntax.init()
    3.27 -  def current_syntax(): Outer_Syntax = syntax
    3.28 +  @volatile private var prover_syntax =
    3.29 +    Outer_Syntax.init() +
    3.30 +      // FIXME avoid hardwired stuff!?
    3.31 +      ("hence", Keyword.PRF_ASM_GOAL, "then have") +
    3.32 +      ("thus", Keyword.PRF_ASM_GOAL, "then show")
    3.33  
    3.34    private val syslog = Volatile(Queue.empty[XML.Elem])
    3.35    def current_syslog(): String = cat_lines(syslog().iterator.map(msg => XML.content(msg).mkString))
    3.36 @@ -135,6 +138,7 @@
    3.37  
    3.38    private val global_state = Volatile(Document.State.init)
    3.39    def current_state(): Document.State = global_state()
    3.40 +  def recent_syntax(): Outer_Syntax = current_state().recent_stable.version.get_finished.syntax
    3.41  
    3.42    def snapshot(name: Document.Node.Name = Document.Node.Name.empty,
    3.43        pending_edits: List[Text.Edit] = Nil): Document.Snapshot =
    3.44 @@ -279,7 +283,6 @@
    3.45          header: Document.Node_Header, edits: List[Document.Node.Edit[Text.Edit, Text.Perspective]])
    3.46      //{{{
    3.47      {
    3.48 -      val syntax = current_syntax()
    3.49        val previous = global_state().history.tip.version
    3.50  
    3.51        prover.get.cancel_execution()
    3.52 @@ -288,7 +291,7 @@
    3.53        val version = Future.promise[Document.Version]
    3.54        val change = global_state >>> (_.continue_history(previous, text_edits, version))
    3.55  
    3.56 -      change_parser ! Text_Edits(syntax, name, previous, text_edits, version)
    3.57 +      change_parser ! Text_Edits(name, previous, text_edits, version)
    3.58      }
    3.59      //}}}
    3.60  
    3.61 @@ -398,19 +401,16 @@
    3.62            System.err.println("cancel_scala " + id)  // FIXME actually cancel JVM task
    3.63  
    3.64          case Isabelle_Markup.Ready if output.is_protocol =>
    3.65 -            // FIXME move to ML side (!?)
    3.66 -            syntax += ("hence", Keyword.PRF_ASM_GOAL, "then have")
    3.67 -            syntax += ("thus", Keyword.PRF_ASM_GOAL, "then show")
    3.68              phase = Session.Ready
    3.69  
    3.70          case Isabelle_Markup.Loaded_Theory(name) if output.is_protocol =>
    3.71            thy_load.register_thy(name)
    3.72  
    3.73          case Isabelle_Markup.Command_Decl(name, kind) if output.is_protocol =>
    3.74 -          syntax += (name, kind)
    3.75 +          prover_syntax += (name, kind)
    3.76  
    3.77          case Isabelle_Markup.Keyword_Decl(name) if output.is_protocol =>
    3.78 -          syntax += name
    3.79 +          prover_syntax += name
    3.80  
    3.81          case _ =>
    3.82            if (output.is_exit && phase == Session.Startup) phase = Session.Failed

     4.1 --- a/src/Pure/Thy/thy_syntax.scala	Thu Mar 15 10:16:21 2012 +0100
     4.2 +++ b/src/Pure/Thy/thy_syntax.scala	Thu Mar 15 11:37:56 2012 +0100
     4.3 @@ -136,7 +136,7 @@
     4.4    {
     4.5      val nodes = previous.nodes
     4.6      val (perspective, new_nodes) = update_perspective(nodes, name, text_perspective)
     4.7 -    val version = Document.Version.make(new_nodes getOrElse nodes)
     4.8 +    val version = Document.Version.make(previous.syntax, new_nodes getOrElse nodes)
     4.9      (perspective, version)
    4.10    }
    4.11  
    4.12 @@ -265,7 +265,7 @@
    4.13                nodes = nodes1
    4.14            }
    4.15        }
    4.16 -      (doc_edits.toList, Document.Version.make(nodes))
    4.17 +      (doc_edits.toList, Document.Version.make(syntax, nodes))
    4.18      }
    4.19    }
    4.20  }

     5.1 --- a/src/Tools/jEdit/src/isabelle_sidekick.scala	Thu Mar 15 10:16:21 2012 +0100
     5.2 +++ b/src/Tools/jEdit/src/isabelle_sidekick.scala	Thu Mar 15 11:37:56 2012 +0100
     5.3 @@ -92,7 +92,7 @@
     5.4            val start = buffer.getLineStartOffset(line)
     5.5            val text = buffer.getSegment(start, caret - start)
     5.6  
     5.7 -          val completion = model.session.current_syntax().completion
     5.8 +          val completion = model.session.recent_syntax().completion
     5.9            completion.complete(text) match {
    5.10              case None => null
    5.11              case Some((word, cs)) =>
    5.12 @@ -116,7 +116,7 @@
    5.13  
    5.14    def parser(data: SideKickParsedData, model: Document_Model)
    5.15    {
    5.16 -    val syntax = model.session.current_syntax()
    5.17 +    val syntax = model.session.recent_syntax()
    5.18  
    5.19      def make_tree(offset: Text.Offset, entry: Structure.Entry): List[DefaultMutableTreeNode] =
    5.20        entry match {

     6.1 --- a/src/Tools/jEdit/src/token_markup.scala	Thu Mar 15 10:16:21 2012 +0100
     6.2 +++ b/src/Tools/jEdit/src/token_markup.scala	Thu Mar 15 11:37:56 2012 +0100
     6.3 @@ -178,7 +178,7 @@
     6.4        {
     6.5          val (styled_tokens, context1) =
     6.6            if (line_ctxt.isDefined && Isabelle.session.is_ready) {
     6.7 -            val syntax = Isabelle.session.current_syntax()
     6.8 +            val syntax = Isabelle.session.recent_syntax()
     6.9              val (tokens, ctxt1) = syntax.scan_context(line, line_ctxt.get)
    6.10              val styled_tokens =
    6.11                tokens.map(tok => (Isabelle_Rendering.token_markup(syntax, tok), tok))