clarified initialization of Thy_Load, Thy_Info, Session;

--- a/src/Pure/Isar/outer_syntax.scala	Tue Aug 21 11:00:54 2012 +0200
+++ b/src/Pure/Isar/outer_syntax.scala	Tue Aug 21 12:15:25 2012 +0200
@@ -35,7 +35,11 @@
   }
 
   val empty: Outer_Syntax = new Outer_Syntax()
+
   def init(): Outer_Syntax = new Outer_Syntax(completion = Completion.init())
+
+  def init_pure(): Outer_Syntax =
+    init() + ("theory", Keyword.THY_BEGIN) + ("ML_file", Keyword.THY_LOAD)
 }
 
 final class Outer_Syntax private(

--- a/src/Pure/System/build.scala	Tue Aug 21 11:00:54 2012 +0200
+++ b/src/Pure/System/build.scala	Tue Aug 21 12:15:25 2012 +0200
@@ -333,20 +333,13 @@
       { case (deps, (name, info)) =>
           val (preloaded, parent_syntax, parent_errors) =
             info.parent match {
+              case None =>
+                (Set.empty[String], Outer_Syntax.init_pure(), Nil)
               case Some(parent_name) =>
                 val parent = deps(parent_name)
                 (parent.loaded_theories, parent.syntax, parent.errors)
-              case None =>
-                val init_syntax =
-                  Outer_Syntax.init() +
-                    // FIXME avoid hardwired stuff!?
-                    ("theory", Keyword.THY_BEGIN) +
-                    ("ML_file", Keyword.THY_LOAD) +
-                    ("hence", (Keyword.PRF_ASM_GOAL, Nil), "then have") +
-                    ("thus", (Keyword.PRF_ASM_GOAL, Nil), "then show")
-                (Set.empty[String], init_syntax, Nil)
             }
-          val thy_info = new Thy_Info(new Thy_Load(preloaded))
+          val thy_info = new Thy_Info(new Thy_Load(preloaded, parent_syntax))
 
           if (verbose) {
             val groups =
@@ -361,7 +354,15 @@
                 map(thy => Document.Node.Name(info.dir + Thy_Load.thy_path(thy))))
 
           val loaded_theories = preloaded ++ thy_deps.map(_._1.theory)
-          val syntax = (parent_syntax /: thy_deps) { case (syn, (_, h)) => syn.add_keywords(h) }
+          val syntax0 = (parent_syntax /: thy_deps) { case (syn, (_, h)) => syn.add_keywords(h) }
+          val syntax =
+            // FIXME avoid hardwired stuff!?
+            // FIXME broken?!
+            if (name == "Pure")
+              syntax0 +
+                ("hence", (Keyword.PRF_ASM_GOAL, Nil), "then have") +
+                ("thus", (Keyword.PRF_ASM_GOAL, Nil), "then show")
+            else syntax0
 
           val all_files =
             thy_deps.map({ case (n, h) =>

--- a/src/Pure/System/session.scala	Tue Aug 21 11:00:54 2012 +0200
+++ b/src/Pure/System/session.scala	Tue Aug 21 12:15:25 2012 +0200
@@ -37,7 +37,7 @@
 }
 
 
-class Session(val thy_load: Thy_Load = new Thy_Load())
+class Session(val thy_load: Thy_Load)
 {
   /* global flags */
 
@@ -108,7 +108,7 @@
           val prev = previous.get_finished
           val (doc_edits, version) =
             Timing.timeit("Thy_Syntax.text_edits", timing) {
-              Thy_Syntax.text_edits(base_syntax, prev, text_edits)
+              Thy_Syntax.text_edits(thy_load.base_syntax, prev, text_edits)
             }
           version_result.fulfill(version)
           sender ! Change(doc_edits, prev, version)
@@ -125,8 +125,6 @@
 
   /* global state */
 
-  @volatile private var base_syntax = Outer_Syntax.init()
-
   private val syslog = Volatile(Queue.empty[XML.Elem])
   def current_syslog(): String = cat_lines(syslog().iterator.map(msg => XML.content(msg).mkString))
 
@@ -145,7 +143,7 @@
   def recent_syntax(): Outer_Syntax =
   {
     val version = current_state().recent_finished.version.get_finished
-    if (version.is_init) base_syntax
+    if (version.is_init) thy_load.base_syntax
     else version.syntax
   }
   def get_recent_syntax(): Option[Outer_Syntax] =
@@ -162,7 +160,7 @@
   def header_edit(name: Document.Node.Name, header: Document.Node.Header): Document.Edit_Text =
   {
     val header1 =
-      if (thy_load.is_loaded(name.theory))
+      if (thy_load.loaded_theories(name.theory))
         header.error("Attempt to update loaded theory " + quote(name.theory))
       else header
     (name, Document.Node.Deps(header1))
@@ -171,7 +169,7 @@
 
   /* actor messages */
 
-  private case class Start(dirs: List[Path], logic: String, args: List[String])
+  private case class Start(args: List[String])
   private case object Cancel_Execution
   private case class Edit(edits: List[Document.Edit_Text])
   private case class Change(
@@ -377,15 +375,9 @@
       receiveWithin(delay_commands_changed.flush_timeout) {
         case TIMEOUT => delay_commands_changed.flush()
 
-        case Start(dirs, name, args) if prover.isEmpty =>
+        case Start(args) if prover.isEmpty =>
           if (phase == Session.Inactive || phase == Session.Failed) {
             phase = Session.Startup
-
-            // FIXME static init in main constructor
-            val content = Build.session_content(dirs, name).check_errors
-            thy_load.register_thys(content.loaded_theories)
-            base_syntax = content.syntax
-
             prover = Some(new Isabelle_Process(receiver.invoke _, args) with Protocol)
           }
 
@@ -440,8 +432,8 @@
 
   /* actions */
 
-  def start(dirs: List[Path], name: String, args: List[String])
-  { session_actor ! Start(dirs, name, args) }
+  def start(args: List[String])
+  { session_actor ! Start(args) }
 
   def stop() { commands_changed_buffer !? Stop; change_parser !? Stop; session_actor !? Stop }
 

--- a/src/Pure/Thy/thy_info.scala	Tue Aug 21 11:00:54 2012 +0200
+++ b/src/Pure/Thy/thy_info.scala	Tue Aug 21 12:15:25 2012 +0200
@@ -36,7 +36,7 @@
   {
     val (deps, seen) = required
     if (seen(name)) required
-    else if (thy_load.is_loaded(name.theory)) (deps, seen + name)
+    else if (thy_load.loaded_theories(name.theory)) (deps, seen + name)
     else {
       try {
         if (initiators.contains(name)) error(cycle_msg(initiators))

--- a/src/Pure/Thy/thy_load.scala	Tue Aug 21 11:00:54 2012 +0200
+++ b/src/Pure/Thy/thy_load.scala	Tue Aug 21 12:15:25 2012 +0200
@@ -20,22 +20,8 @@
 }
 
 
-class Thy_Load(preloaded: Set[String] = Set.empty)
+class Thy_Load(val loaded_theories: Set[String] = Set.empty, val base_syntax: Outer_Syntax)
 {
-  /* loaded theories provided by prover */
-
-  private var loaded_theories: Set[String] = preloaded
-
-  def register_thy(name: String): Unit =
-    synchronized { loaded_theories += name }
-
-  def register_thys(names: Set[String]): Unit =
-    synchronized { loaded_theories ++= names }
-
-  def is_loaded(thy_name: String): Boolean =
-    synchronized { loaded_theories.contains(thy_name) }
-
-
   /* file-system operations */
 
   def append(dir: String, source_path: Path): String =
@@ -54,7 +40,7 @@
   private def import_name(dir: String, s: String): Document.Node.Name =
   {
     val theory = Thy_Header.base_name(s)
-    if (is_loaded(theory)) Document.Node.Name(theory, "", theory)
+    if (loaded_theories(theory)) Document.Node.Name(theory, "", theory)
     else {
       val path = Path.explode(s)
       val node = append(dir, Thy_Load.thy_path(path))

--- a/src/Tools/jEdit/src/jedit_thy_load.scala	Tue Aug 21 11:00:54 2012 +0200
+++ b/src/Tools/jEdit/src/jedit_thy_load.scala	Tue Aug 21 12:15:25 2012 +0200
@@ -17,7 +17,8 @@
 import org.gjt.sp.jedit.View
 
 
-class JEdit_Thy_Load extends Thy_Load()
+class JEdit_Thy_Load(loaded_theories: Set[String] = Set.empty, base_syntax: Outer_Syntax)
+  extends Thy_Load(loaded_theories, base_syntax)
 {
   override def append(dir: String, source_path: Path): String =
   {

--- a/src/Tools/jEdit/src/plugin.scala	Tue Aug 21 11:00:54 2012 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Tue Aug 21 12:15:25 2012 +0200
@@ -37,8 +37,8 @@
   var plugin: Plugin = null
   var session: Session = null
 
-  val thy_load = new JEdit_Thy_Load
-  val thy_info = new Thy_Info(thy_load)
+  def thy_load(): JEdit_Thy_Load =
+    session.thy_load.asInstanceOf[JEdit_Thy_Load]
 
 
   /* properties */
@@ -298,17 +298,22 @@
     component
   }
 
-  def start_session()
+  def session_args(): List[String] =
   {
-    val dirs = Path.split(Isabelle_System.getenv("JEDIT_SESSION_DIRS"))
     val modes = space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE")).map("-m" + _)
     val logic = {
       val logic = Property("logic")
       if (logic != null && logic != "") logic
       else Isabelle.default_logic()
     }
-    val name = Path.explode(logic).base.implode  // FIXME more robust session name
-    session.start(dirs, name, modes ::: List(logic))
+    modes ::: List(logic)
+  }
+
+  def session_content(): Build.Session_Content =
+  {
+    val dirs = Path.split(Isabelle_System.getenv("JEDIT_SESSION_DIRS"))
+    val name = Path.explode(session_args().last).base.implode  // FIXME more robust
+    Build.session_content(dirs, name).check_errors
   }
 
 
@@ -359,8 +364,9 @@
           for (buffer <- buffers; model <- Isabelle.document_model(buffer))
             yield model.name
 
+        val thy_info = new Thy_Info(Isabelle.thy_load)
         // FIXME avoid I/O in Swing thread!?!
-        val files = Isabelle.thy_info.dependencies(thys).map(_._1.node).
+        val files = thy_info.dependencies(thys).map(_._1.node).
           filter(file => !loaded_buffer(file) && Isabelle.thy_load.check_file(view, file))
 
         if (!files.isEmpty) {
@@ -422,7 +428,7 @@
     message match {
       case msg: EditorStarted =>
         if (Isabelle.Boolean_Property("auto-start"))
-          Isabelle.start_session()
+          Isabelle.session.start(Isabelle.session_args())
 
       case msg: BufferUpdate
       if msg.getWhat == BufferUpdate.LOADED || msg.getWhat == BufferUpdate.PROPERTIES_CHANGED =>
@@ -459,12 +465,16 @@
   }
 
   override def start()
-  {
+  { // FIXME more robust error handling
     Isabelle.plugin = this
     Isabelle.setup_tooltips()
     Isabelle_System.init()
     Isabelle_System.install_fonts()
-    Isabelle.session = new Session(Isabelle.thy_load)
+
+    val content = Isabelle.session_content()
+    val thy_load = new JEdit_Thy_Load(content.loaded_theories, content.syntax)
+    Isabelle.session = new Session(thy_load)
+
     SyntaxUtilities.setStyleExtender(new Token_Markup.Style_Extender)
     if (ModeProvider.instance.isInstanceOf[ModeProvider])
       ModeProvider.instance = new Token_Markup.Mode_Provider(ModeProvider.instance)

--- a/src/Tools/jEdit/src/session_dockable.scala	Tue Aug 21 11:00:54 2012 +0200
+++ b/src/Tools/jEdit/src/session_dockable.scala	Tue Aug 21 12:15:25 2012 +0200
@@ -134,7 +134,7 @@
         }
       val nodes_status1 =
         (nodes_status /: iterator)({ case (status, (name, node)) =>
-            if (Isabelle.thy_load.is_loaded(name.theory)) status
+            if (Isabelle.thy_load.loaded_theories(name.theory)) status
             else status + (name -> Protocol.node_status(snapshot.state, snapshot.version, node)) })
 
       if (nodes_status != nodes_status1) {