prefer static Build.outer_syntax in Isabelle/Scala session -- discontinued incremental protocol;
authorwenzelm
Tue Aug 07 16:34:15 2012 +0200 (2012-08-07)
changeset 48709719f458cd89e
parent 48708 189ece4b4ff1
child 48710 5b51ccdc8623
prefer static Build.outer_syntax in Isabelle/Scala session -- discontinued incremental protocol;
just one cumulative Keyword.status at end of batch session;
Admin/update-keywords
etc/isar-keywords-ZF.el
etc/isar-keywords.el
src/Pure/Isar/keyword.ML
src/Pure/PIDE/isabelle_markup.ML
src/Pure/PIDE/isabelle_markup.scala
src/Pure/System/isabelle_process.ML
src/Pure/System/session.ML
src/Pure/System/session.scala
src/Tools/jEdit/src/plugin.scala
     1.1 --- a/Admin/update-keywords	Tue Aug 07 15:19:08 2012 +0200
     1.2 +++ b/Admin/update-keywords	Tue Aug 07 16:34:15 2012 +0200
     1.3 @@ -11,10 +11,8 @@
     1.4  cd "$ISABELLE_HOME/etc"
     1.5  
     1.6  isabelle keywords \
     1.7 -  "$LOG/Pure.gz" "$LOG/HOL.gz" "$LOG/HOLCF.gz" "$LOG/HOL-Boogie.gz" \
     1.8 -  "$LOG/HOL-Library.gz" "$LOG/HOL-Nominal.gz" "$LOG/HOL-Statespace.gz" \
     1.9 -  "$LOG/HOL-SPARK.gz" "$LOG/HOL-TPTP.gz" "$LOG/HOL-Import.gz"
    1.10 +  "$LOG/HOLCF.gz" "$LOG/HOL-Boogie.gz" "$LOG/HOL-Library.gz" "$LOG/HOL-Nominal.gz" \
    1.11 +  "$LOG/HOL-Statespace.gz" "$LOG/HOL-SPARK.gz" "$LOG/HOL-TPTP.gz" "$LOG/HOL-Import.gz"
    1.12  
    1.13 -isabelle keywords -k ZF \
    1.14 -  "$LOG/Pure.gz" "$LOG/FOL.gz" "$LOG/ZF.gz"
    1.15 +isabelle keywords -k ZF "$LOG/ZF.gz"
    1.16  
     2.1 --- a/etc/isar-keywords-ZF.el	Tue Aug 07 15:19:08 2012 +0200
     2.2 +++ b/etc/isar-keywords-ZF.el	Tue Aug 07 16:34:15 2012 +0200
     2.3 @@ -1,6 +1,6 @@
     2.4  ;;
     2.5  ;; Keyword classification tables for Isabelle/Isar.
     2.6 -;; Generated from Pure + FOL + ZF.
     2.7 +;; Generated from ZF.
     2.8  ;; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT ***
     2.9  ;;
    2.10  
     3.1 --- a/etc/isar-keywords.el	Tue Aug 07 15:19:08 2012 +0200
     3.2 +++ b/etc/isar-keywords.el	Tue Aug 07 16:34:15 2012 +0200
     3.3 @@ -1,6 +1,6 @@
     3.4  ;;
     3.5  ;; Keyword classification tables for Isabelle/Isar.
     3.6 -;; Generated from Pure + HOL + HOLCF + HOL-Boogie + HOL-Library + HOL-Nominal + HOL-Statespace + HOL-SPARK + HOL-TPTP + HOL-Import.
     3.7 +;; Generated from HOLCF + HOL-Boogie + HOL-Library + HOL-Nominal + HOL-Statespace + HOL-SPARK + HOL-TPTP + HOL-Import.
     3.8  ;; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT ***
     3.9  ;;
    3.10  
     4.1 --- a/src/Pure/Isar/keyword.ML	Tue Aug 07 15:19:08 2012 +0200
     4.2 +++ b/src/Pure/Isar/keyword.ML	Tue Aug 07 16:34:15 2012 +0200
     4.3 @@ -49,7 +49,6 @@
     4.4    val command_keyword: string -> T option
     4.5    val command_tags: string -> string list
     4.6    val dest: unit -> string list * string list
     4.7 -  val keyword_statusN: string
     4.8    val status: unit -> unit
     4.9    val define: string * T option -> unit
    4.10    val is_diag: string -> bool
    4.11 @@ -183,43 +182,29 @@
    4.12  
    4.13  (* status *)
    4.14  
    4.15 -val keyword_statusN = "keyword_status";
    4.16 -
    4.17 -fun status_message m s =
    4.18 -  Position.setmp_thread_data Position.none
    4.19 -    (if print_mode_active keyword_statusN then Output.protocol_message m else writeln) s;
    4.20 -
    4.21 -fun keyword_status name =
    4.22 -  status_message (Isabelle_Markup.keyword_decl name)
    4.23 -    ("Outer syntax keyword " ^ quote name);
    4.24 -
    4.25 -fun command_status (name, kind) =
    4.26 -  status_message (Isabelle_Markup.command_decl name (kind_of kind))
    4.27 -    ("Outer syntax keyword " ^ quote name ^ " :: " ^ kind_of kind);
    4.28 -
    4.29  fun status () =
    4.30    let
    4.31      val {lexicons = (minor, _), commands} = get_keywords ();
    4.32 -    val _ = List.app keyword_status (sort_strings (Scan.dest_lexicon minor));
    4.33 -    val _ = List.app command_status (sort_wrt #1 (Symtab.dest commands));
    4.34 +    val _ = sort_strings (Scan.dest_lexicon minor) |> List.app (fn name =>
    4.35 +      writeln ("Outer syntax keyword " ^ quote name));
    4.36 +    val _ = sort_wrt #1 (Symtab.dest commands) |> List.app (fn (name, kind) =>
    4.37 +      writeln ("Outer syntax keyword " ^ quote name ^ " :: " ^ kind_of kind));
    4.38    in () end;
    4.39  
    4.40  
    4.41  (* define *)
    4.42  
    4.43 -fun define (name, NONE) =
    4.44 -     (change_keywords (fn ((minor, major), commands) =>
    4.45 -        let
    4.46 -          val minor' = Scan.extend_lexicon (Symbol.explode name) minor;
    4.47 -        in ((minor', major), commands) end);
    4.48 -      keyword_status name)
    4.49 -  | define (name, SOME kind) =
    4.50 -     (change_keywords (fn ((minor, major), commands) =>
    4.51 -        let
    4.52 -          val major' = Scan.extend_lexicon (Symbol.explode name) major;
    4.53 -          val commands' = Symtab.update (name, kind) commands;
    4.54 -        in ((minor, major'), commands') end);
    4.55 -      command_status (name, kind));
    4.56 +fun define (name, opt_kind) = change_keywords (fn ((minor, major), commands) =>
    4.57 +  (case opt_kind of
    4.58 +    NONE =>
    4.59 +      let
    4.60 +        val minor' = Scan.extend_lexicon (Symbol.explode name) minor;
    4.61 +      in ((minor', major), commands) end
    4.62 +  | SOME kind =>
    4.63 +      let
    4.64 +        val major' = Scan.extend_lexicon (Symbol.explode name) major;
    4.65 +        val commands' = Symtab.update (name, kind) commands;
    4.66 +      in ((minor, major'), commands') end));
    4.67  
    4.68  
    4.69  (* command categories *)
     5.1 --- a/src/Pure/PIDE/isabelle_markup.ML	Tue Aug 07 15:19:08 2012 +0200
     5.2 +++ b/src/Pure/PIDE/isabelle_markup.ML	Tue Aug 07 16:34:15 2012 +0200
     5.3 @@ -104,8 +104,6 @@
     5.4    val functionN: string
     5.5    val ready: Properties.T
     5.6    val loaded_theory: string -> Properties.T
     5.7 -  val keyword_decl: string -> Properties.T
     5.8 -  val command_decl: string -> string -> Properties.T
     5.9    val assign_execs: Properties.T
    5.10    val removed_versions: Properties.T
    5.11    val invoke_scala: string -> string -> Properties.T
    5.12 @@ -312,10 +310,6 @@
    5.13  
    5.14  fun loaded_theory name = [(functionN, "loaded_theory"), (Markup.nameN, name)];
    5.15  
    5.16 -fun keyword_decl name = [(functionN, "keyword_decl"), (Markup.nameN, name)];
    5.17 -fun command_decl name kind =
    5.18 -  [(functionN, "command_decl"), (Markup.nameN, name), (Markup.kindN, kind)];
    5.19 -
    5.20  val assign_execs = [(functionN, "assign_execs")];
    5.21  val removed_versions = [(functionN, "removed_versions")];
    5.22  
     6.1 --- a/src/Pure/PIDE/isabelle_markup.scala	Tue Aug 07 15:19:08 2012 +0200
     6.2 +++ b/src/Pure/PIDE/isabelle_markup.scala	Tue Aug 07 16:34:15 2012 +0200
     6.3 @@ -261,24 +261,6 @@
     6.4        }
     6.5    }
     6.6  
     6.7 -  object Keyword_Decl
     6.8 -  {
     6.9 -    def unapply(props: Properties.T): Option[String] =
    6.10 -      props match {
    6.11 -        case List((FUNCTION, "keyword_decl"), (Markup.NAME, name)) => Some(name)
    6.12 -        case _ => None
    6.13 -      }
    6.14 -  }
    6.15 -  object Command_Decl
    6.16 -  {
    6.17 -    def unapply(props: Properties.T): Option[(String, String)] =
    6.18 -      props match {
    6.19 -        case List((FUNCTION, "command_decl"), (Markup.NAME, name), (Markup.KIND, kind)) =>
    6.20 -          Some((name, kind))
    6.21 -        case _ => None
    6.22 -      }
    6.23 -  }
    6.24 -
    6.25    val Assign_Execs: Properties.T = List((FUNCTION, "assign_execs"))
    6.26    val Removed_Versions: Properties.T = List((FUNCTION, "removed_versions"))
    6.27  
     7.1 --- a/src/Pure/System/isabelle_process.ML	Tue Aug 07 15:19:08 2012 +0200
     7.2 +++ b/src/Pure/System/isabelle_process.ML	Tue Aug 07 16:34:15 2012 +0200
     7.3 @@ -178,13 +178,11 @@
     7.4        Unsynchronized.change print_mode
     7.5          (fn mode =>
     7.6            (mode @ [Syntax_Trans.no_bracketsN, Syntax_Trans.no_type_bracketsN])
     7.7 -          |> fold (update op =)
     7.8 -            [Symbol.xsymbolsN, isabelle_processN, Keyword.keyword_statusN, Pretty.symbolicN]);
     7.9 +          |> fold (update op =) [Symbol.xsymbolsN, isabelle_processN, Pretty.symbolicN]);
    7.10  
    7.11      val channel = rendezvous ();
    7.12      val _ = setup_channels channel;
    7.13  
    7.14 -    val _ = Keyword.status ();
    7.15      val _ = Thy_Info.status ();
    7.16      val _ = Output.protocol_message Isabelle_Markup.ready "";
    7.17    in loop channel end));
     8.1 --- a/src/Pure/System/session.ML	Tue Aug 07 15:19:08 2012 +0200
     8.2 +++ b/src/Pure/System/session.ML	Tue Aug 07 16:34:15 2012 +0200
     8.3 @@ -71,6 +71,7 @@
     8.4  fun finish () =
     8.5    (Thy_Info.finish ();
     8.6      Present.finish ();
     8.7 +    Keyword.status ();
     8.8      Outer_Syntax.check_syntax ();
     8.9      Future.shutdown ();
    8.10      Options.reset_default ();
     9.1 --- a/src/Pure/System/session.scala	Tue Aug 07 15:19:08 2012 +0200
     9.2 +++ b/src/Pure/System/session.scala	Tue Aug 07 16:34:15 2012 +0200
     9.3 @@ -108,7 +108,7 @@
     9.4            val prev = previous.get_finished
     9.5            val (doc_edits, version) =
     9.6              Timing.timeit("Thy_Syntax.text_edits", timing) {
     9.7 -              Thy_Syntax.text_edits(prover_syntax, prev, text_edits)
     9.8 +              Thy_Syntax.text_edits(base_syntax, prev, text_edits)
     9.9              }
    9.10            version_result.fulfill(version)
    9.11            sender ! Change(doc_edits, prev, version)
    9.12 @@ -125,11 +125,7 @@
    9.13  
    9.14    /* global state */
    9.15  
    9.16 -  @volatile private var prover_syntax =
    9.17 -    Outer_Syntax.init() +
    9.18 -      // FIXME avoid hardwired stuff!?
    9.19 -      ("hence", Keyword.PRF_ASM_GOAL, "then have") +
    9.20 -      ("thus", Keyword.PRF_ASM_GOAL, "then show")
    9.21 +  @volatile private var base_syntax = Outer_Syntax.empty
    9.22  
    9.23    private val syslog = Volatile(Queue.empty[XML.Elem])
    9.24    def current_syslog(): String = cat_lines(syslog().iterator.map(msg => XML.content(msg).mkString))
    9.25 @@ -149,7 +145,7 @@
    9.26    def recent_syntax(): Outer_Syntax =
    9.27    {
    9.28      val version = current_state().recent_finished.version.get_finished
    9.29 -    if (version.is_init) prover_syntax
    9.30 +    if (version.is_init) base_syntax
    9.31      else version.syntax
    9.32    }
    9.33  
    9.34 @@ -172,7 +168,7 @@
    9.35  
    9.36    /* actor messages */
    9.37  
    9.38 -  private case class Start(args: List[String])
    9.39 +  private case class Start(logic: String, args: List[String])
    9.40    private case object Cancel_Execution
    9.41    private case class Edit(edits: List[Document.Edit_Text])
    9.42    private case class Change(
    9.43 @@ -361,12 +357,6 @@
    9.44          case Isabelle_Markup.Loaded_Theory(name) if output.is_protocol =>
    9.45            thy_load.register_thy(name)
    9.46  
    9.47 -        case Isabelle_Markup.Command_Decl(name, kind) if output.is_protocol =>
    9.48 -          prover_syntax += (name, kind)
    9.49 -
    9.50 -        case Isabelle_Markup.Keyword_Decl(name) if output.is_protocol =>
    9.51 -          prover_syntax += name
    9.52 -
    9.53          case Isabelle_Markup.Return_Code(rc) if output.is_exit =>
    9.54            if (rc == 0) phase = Session.Inactive
    9.55            else phase = Session.Failed
    9.56 @@ -387,9 +377,10 @@
    9.57        receiveWithin(delay_commands_changed.flush_timeout) {
    9.58          case TIMEOUT => delay_commands_changed.flush()
    9.59  
    9.60 -        case Start(args) if prover.isEmpty =>
    9.61 +        case Start(name, args) if prover.isEmpty =>
    9.62            if (phase == Session.Inactive || phase == Session.Failed) {
    9.63              phase = Session.Startup
    9.64 +            base_syntax = Build.outer_syntax(name)
    9.65              prover = Some(new Isabelle_Process(receiver.invoke _, args) with Protocol)
    9.66            }
    9.67  
    9.68 @@ -444,7 +435,7 @@
    9.69  
    9.70    /* actions */
    9.71  
    9.72 -  def start(args: List[String]) { session_actor ! Start(args) }
    9.73 +  def start(name: String, args: List[String]) { session_actor ! Start(name, args) }
    9.74  
    9.75    def stop() { commands_changed_buffer !? Stop; change_parser !? Stop; session_actor !? Stop }
    9.76  
    10.1 --- a/src/Tools/jEdit/src/plugin.scala	Tue Aug 07 15:19:08 2012 +0200
    10.2 +++ b/src/Tools/jEdit/src/plugin.scala	Tue Aug 07 16:34:15 2012 +0200
    10.3 @@ -301,7 +301,8 @@
    10.4        if (logic != null && logic != "") logic
    10.5        else Isabelle.default_logic()
    10.6      }
    10.7 -    session.start(modes ::: List(logic))
    10.8 +    val name = Path.explode(logic).base.implode  // FIXME more robust session name
    10.9 +    session.start(name, modes ::: List(logic))
   10.10    }
   10.11  
   10.12