# HG changeset patch
# User wenzelm
# Date 1344350055 -7200
# Node ID 719f458cd89ea582a34b1ac12c6125228fb4f227
# Parent  189ece4b4ff11db7b70417dd0f8e00b6bdf23ddd
prefer static Build.outer_syntax in Isabelle/Scala session -- discontinued incremental protocol;
just one cumulative Keyword.status at end of batch session;

diff -r 189ece4b4ff1 -r 719f458cd89e Admin/update-keywords
--- a/Admin/update-keywords	Tue Aug 07 15:19:08 2012 +0200
+++ b/Admin/update-keywords	Tue Aug 07 16:34:15 2012 +0200
@@ -11,10 +11,8 @@
 cd "$ISABELLE_HOME/etc"
 
 isabelle keywords \
-  "$LOG/Pure.gz" "$LOG/HOL.gz" "$LOG/HOLCF.gz" "$LOG/HOL-Boogie.gz" \
-  "$LOG/HOL-Library.gz" "$LOG/HOL-Nominal.gz" "$LOG/HOL-Statespace.gz" \
-  "$LOG/HOL-SPARK.gz" "$LOG/HOL-TPTP.gz" "$LOG/HOL-Import.gz"
+  "$LOG/HOLCF.gz" "$LOG/HOL-Boogie.gz" "$LOG/HOL-Library.gz" "$LOG/HOL-Nominal.gz" \
+  "$LOG/HOL-Statespace.gz" "$LOG/HOL-SPARK.gz" "$LOG/HOL-TPTP.gz" "$LOG/HOL-Import.gz"
 
-isabelle keywords -k ZF \
-  "$LOG/Pure.gz" "$LOG/FOL.gz" "$LOG/ZF.gz"
+isabelle keywords -k ZF "$LOG/ZF.gz"
 
diff -r 189ece4b4ff1 -r 719f458cd89e etc/isar-keywords-ZF.el
--- a/etc/isar-keywords-ZF.el	Tue Aug 07 15:19:08 2012 +0200
+++ b/etc/isar-keywords-ZF.el	Tue Aug 07 16:34:15 2012 +0200
@@ -1,6 +1,6 @@
 ;;
 ;; Keyword classification tables for Isabelle/Isar.
-;; Generated from Pure + FOL + ZF.
+;; Generated from ZF.
 ;; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT ***
 ;;
 
diff -r 189ece4b4ff1 -r 719f458cd89e etc/isar-keywords.el
--- a/etc/isar-keywords.el	Tue Aug 07 15:19:08 2012 +0200
+++ b/etc/isar-keywords.el	Tue Aug 07 16:34:15 2012 +0200
@@ -1,6 +1,6 @@
 ;;
 ;; Keyword classification tables for Isabelle/Isar.
-;; Generated from Pure + HOL + HOLCF + HOL-Boogie + HOL-Library + HOL-Nominal + HOL-Statespace + HOL-SPARK + HOL-TPTP + HOL-Import.
+;; Generated from HOLCF + HOL-Boogie + HOL-Library + HOL-Nominal + HOL-Statespace + HOL-SPARK + HOL-TPTP + HOL-Import.
 ;; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT ***
 ;;
 
diff -r 189ece4b4ff1 -r 719f458cd89e src/Pure/Isar/keyword.ML
--- a/src/Pure/Isar/keyword.ML	Tue Aug 07 15:19:08 2012 +0200
+++ b/src/Pure/Isar/keyword.ML	Tue Aug 07 16:34:15 2012 +0200
@@ -49,7 +49,6 @@
   val command_keyword: string -> T option
   val command_tags: string -> string list
   val dest: unit -> string list * string list
-  val keyword_statusN: string
   val status: unit -> unit
   val define: string * T option -> unit
   val is_diag: string -> bool
@@ -183,43 +182,29 @@
 
 (* status *)
 
-val keyword_statusN = "keyword_status";
-
-fun status_message m s =
-  Position.setmp_thread_data Position.none
-    (if print_mode_active keyword_statusN then Output.protocol_message m else writeln) s;
-
-fun keyword_status name =
-  status_message (Isabelle_Markup.keyword_decl name)
-    ("Outer syntax keyword " ^ quote name);
-
-fun command_status (name, kind) =
-  status_message (Isabelle_Markup.command_decl name (kind_of kind))
-    ("Outer syntax keyword " ^ quote name ^ " :: " ^ kind_of kind);
-
 fun status () =
   let
     val {lexicons = (minor, _), commands} = get_keywords ();
-    val _ = List.app keyword_status (sort_strings (Scan.dest_lexicon minor));
-    val _ = List.app command_status (sort_wrt #1 (Symtab.dest commands));
+    val _ = sort_strings (Scan.dest_lexicon minor) |> List.app (fn name =>
+      writeln ("Outer syntax keyword " ^ quote name));
+    val _ = sort_wrt #1 (Symtab.dest commands) |> List.app (fn (name, kind) =>
+      writeln ("Outer syntax keyword " ^ quote name ^ " :: " ^ kind_of kind));
   in () end;
 
 
 (* define *)
 
-fun define (name, NONE) =
-     (change_keywords (fn ((minor, major), commands) =>
-        let
-          val minor' = Scan.extend_lexicon (Symbol.explode name) minor;
-        in ((minor', major), commands) end);
-      keyword_status name)
-  | define (name, SOME kind) =
-     (change_keywords (fn ((minor, major), commands) =>
-        let
-          val major' = Scan.extend_lexicon (Symbol.explode name) major;
-          val commands' = Symtab.update (name, kind) commands;
-        in ((minor, major'), commands') end);
-      command_status (name, kind));
+fun define (name, opt_kind) = change_keywords (fn ((minor, major), commands) =>
+  (case opt_kind of
+    NONE =>
+      let
+        val minor' = Scan.extend_lexicon (Symbol.explode name) minor;
+      in ((minor', major), commands) end
+  | SOME kind =>
+      let
+        val major' = Scan.extend_lexicon (Symbol.explode name) major;
+        val commands' = Symtab.update (name, kind) commands;
+      in ((minor, major'), commands') end));
 
 
 (* command categories *)
diff -r 189ece4b4ff1 -r 719f458cd89e src/Pure/PIDE/isabelle_markup.ML
--- a/src/Pure/PIDE/isabelle_markup.ML	Tue Aug 07 15:19:08 2012 +0200
+++ b/src/Pure/PIDE/isabelle_markup.ML	Tue Aug 07 16:34:15 2012 +0200
@@ -104,8 +104,6 @@
   val functionN: string
   val ready: Properties.T
   val loaded_theory: string -> Properties.T
-  val keyword_decl: string -> Properties.T
-  val command_decl: string -> string -> Properties.T
   val assign_execs: Properties.T
   val removed_versions: Properties.T
   val invoke_scala: string -> string -> Properties.T
@@ -312,10 +310,6 @@
 
 fun loaded_theory name = [(functionN, "loaded_theory"), (Markup.nameN, name)];
 
-fun keyword_decl name = [(functionN, "keyword_decl"), (Markup.nameN, name)];
-fun command_decl name kind =
-  [(functionN, "command_decl"), (Markup.nameN, name), (Markup.kindN, kind)];
-
 val assign_execs = [(functionN, "assign_execs")];
 val removed_versions = [(functionN, "removed_versions")];
 
diff -r 189ece4b4ff1 -r 719f458cd89e src/Pure/PIDE/isabelle_markup.scala
--- a/src/Pure/PIDE/isabelle_markup.scala	Tue Aug 07 15:19:08 2012 +0200
+++ b/src/Pure/PIDE/isabelle_markup.scala	Tue Aug 07 16:34:15 2012 +0200
@@ -261,24 +261,6 @@
       }
   }
 
-  object Keyword_Decl
-  {
-    def unapply(props: Properties.T): Option[String] =
-      props match {
-        case List((FUNCTION, "keyword_decl"), (Markup.NAME, name)) => Some(name)
-        case _ => None
-      }
-  }
-  object Command_Decl
-  {
-    def unapply(props: Properties.T): Option[(String, String)] =
-      props match {
-        case List((FUNCTION, "command_decl"), (Markup.NAME, name), (Markup.KIND, kind)) =>
-          Some((name, kind))
-        case _ => None
-      }
-  }
-
   val Assign_Execs: Properties.T = List((FUNCTION, "assign_execs"))
   val Removed_Versions: Properties.T = List((FUNCTION, "removed_versions"))
 
diff -r 189ece4b4ff1 -r 719f458cd89e src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Tue Aug 07 15:19:08 2012 +0200
+++ b/src/Pure/System/isabelle_process.ML	Tue Aug 07 16:34:15 2012 +0200
@@ -178,13 +178,11 @@
       Unsynchronized.change print_mode
         (fn mode =>
           (mode @ [Syntax_Trans.no_bracketsN, Syntax_Trans.no_type_bracketsN])
-          |> fold (update op =)
-            [Symbol.xsymbolsN, isabelle_processN, Keyword.keyword_statusN, Pretty.symbolicN]);
+          |> fold (update op =) [Symbol.xsymbolsN, isabelle_processN, Pretty.symbolicN]);
 
     val channel = rendezvous ();
     val _ = setup_channels channel;
 
-    val _ = Keyword.status ();
     val _ = Thy_Info.status ();
     val _ = Output.protocol_message Isabelle_Markup.ready "";
   in loop channel end));
diff -r 189ece4b4ff1 -r 719f458cd89e src/Pure/System/session.ML
--- a/src/Pure/System/session.ML	Tue Aug 07 15:19:08 2012 +0200
+++ b/src/Pure/System/session.ML	Tue Aug 07 16:34:15 2012 +0200
@@ -71,6 +71,7 @@
 fun finish () =
   (Thy_Info.finish ();
     Present.finish ();
+    Keyword.status ();
     Outer_Syntax.check_syntax ();
     Future.shutdown ();
     Options.reset_default ();
diff -r 189ece4b4ff1 -r 719f458cd89e src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Tue Aug 07 15:19:08 2012 +0200
+++ b/src/Pure/System/session.scala	Tue Aug 07 16:34:15 2012 +0200
@@ -108,7 +108,7 @@
           val prev = previous.get_finished
           val (doc_edits, version) =
             Timing.timeit("Thy_Syntax.text_edits", timing) {
-              Thy_Syntax.text_edits(prover_syntax, prev, text_edits)
+              Thy_Syntax.text_edits(base_syntax, prev, text_edits)
             }
           version_result.fulfill(version)
           sender ! Change(doc_edits, prev, version)
@@ -125,11 +125,7 @@
 
   /* global state */
 
-  @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")
+  @volatile private var base_syntax = Outer_Syntax.empty
 
   private val syslog = Volatile(Queue.empty[XML.Elem])
   def current_syslog(): String = cat_lines(syslog().iterator.map(msg => XML.content(msg).mkString))
@@ -149,7 +145,7 @@
   def recent_syntax(): Outer_Syntax =
   {
     val version = current_state().recent_finished.version.get_finished
-    if (version.is_init) prover_syntax
+    if (version.is_init) base_syntax
     else version.syntax
   }
 
@@ -172,7 +168,7 @@
 
   /* actor messages */
 
-  private case class Start(args: List[String])
+  private case class Start(logic: String, args: List[String])
   private case object Cancel_Execution
   private case class Edit(edits: List[Document.Edit_Text])
   private case class Change(
@@ -361,12 +357,6 @@
         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 =>
-          prover_syntax += (name, kind)
-
-        case Isabelle_Markup.Keyword_Decl(name) if output.is_protocol =>
-          prover_syntax += name
-
         case Isabelle_Markup.Return_Code(rc) if output.is_exit =>
           if (rc == 0) phase = Session.Inactive
           else phase = Session.Failed
@@ -387,9 +377,10 @@
       receiveWithin(delay_commands_changed.flush_timeout) {
         case TIMEOUT => delay_commands_changed.flush()
 
-        case Start(args) if prover.isEmpty =>
+        case Start(name, args) if prover.isEmpty =>
           if (phase == Session.Inactive || phase == Session.Failed) {
             phase = Session.Startup
+            base_syntax = Build.outer_syntax(name)
             prover = Some(new Isabelle_Process(receiver.invoke _, args) with Protocol)
           }
 
@@ -444,7 +435,7 @@
 
   /* actions */
 
-  def start(args: List[String]) { session_actor ! Start(args) }
+  def start(name: String, args: List[String]) { session_actor ! Start(name, args) }
 
   def stop() { commands_changed_buffer !? Stop; change_parser !? Stop; session_actor !? Stop }
 
diff -r 189ece4b4ff1 -r 719f458cd89e src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Tue Aug 07 15:19:08 2012 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Tue Aug 07 16:34:15 2012 +0200
@@ -301,7 +301,8 @@
       if (logic != null && logic != "") logic
       else Isabelle.default_logic()
     }
-    session.start(modes ::: List(logic))
+    val name = Path.explode(logic).base.implode  // FIXME more robust session name
+    session.start(name, modes ::: List(logic))
   }