merged
authorhaftmann
Sat, 17 Jan 2009 08:30:06 +0100
changeset 29527 7178c11b6bc1
parent 29522 793766d4c1b5 (diff)
parent 29526 0b32c8b84d3e (current diff)
child 29529 70ef35ccdc3b
child 29544 bc50244cd1d7
merged
--- a/src/Pure/General/markup.ML	Sat Jan 17 08:29:54 2009 +0100
+++ b/src/Pure/General/markup.ML	Sat Jan 17 08:30:06 2009 +0100
@@ -95,17 +95,7 @@
   val editN: string val edit: string -> string -> T
   val pidN: string
   val sessionN: string
-  val classN: string
-  val messageN: string val message: string -> T
   val promptN: string val prompt: T
-  val writelnN: string
-  val priorityN: string
-  val tracingN: string
-  val warningN: string
-  val errorN: string
-  val debugN: string
-  val initN: string
-  val statusN: string
   val no_output: output * output
   val default_output: T -> output * output
   val add_mode: string -> (T -> output * output) -> unit
@@ -284,19 +274,8 @@
 val pidN = "pid";
 val sessionN = "session";
 
-val classN = "class";
-val (messageN, message) = markup_string "message" classN;
-
 val (promptN, prompt) = markup_elem "prompt";
 
-val writelnN = "writeln";
-val priorityN = "priority";
-val tracingN = "tracing";
-val warningN = "warning";
-val errorN = "error";
-val debugN = "debug";
-val initN = "init";
-val statusN = "status";
 
 
 (* print mode operations *)
--- a/src/Pure/General/markup.scala	Sat Jan 17 08:29:54 2009 +0100
+++ b/src/Pure/General/markup.scala	Sat Jan 17 08:30:06 2009 +0100
@@ -131,6 +131,21 @@
   val SESSION = "session"
 
   val MESSAGE = "message"
+  val CLASS = "class"
+
+  val INIT = "init"
+  val STATUS = "status"
+  val WRITELN = "writeln"
+  val PRIORITY = "priority"
+  val TRACING = "tracing"
+  val WARNING = "warning"
+  val ERROR = "error"
+  val DEBUG = "debug"
+  val SYSTEM = "system"
+  val STDIN = "stdin"
+  val STDOUT = "stdout"
+  val SIGNAL = "signal"
+  val EXIT = "exit"
 
 
   /* content */
--- a/src/Pure/General/yxml.scala	Sat Jan 17 08:29:54 2009 +0100
+++ b/src/Pure/General/yxml.scala	Sat Jan 17 08:30:06 2009 +0100
@@ -109,12 +109,21 @@
       case _ => err("multiple results")
     }
 
+
+  /* failsafe parsing */
+
+  private def markup_failsafe(source: CharSequence) =
+    XML.Elem (Markup.BAD, Nil,
+      List(XML.Text(source.toString.replace(X_string, "\\<^X>").replace(Y_string, "\\<^Y>"))))
+
+  def parse_body_failsafe(source: CharSequence) = {
+    try { parse_body(source) }
+    catch { case _: RuntimeException => List(markup_failsafe(source)) }
+  }
+
   def parse_failsafe(source: CharSequence) = {
     try { parse(source) }
-    catch {
-      case _: RuntimeException => XML.Elem (Markup.BAD, Nil,
-        List(XML.Text(source.toString.replace(X_string, "\\<^X>").replace(Y_string, "\\<^Y>"))))
-    }
+    catch { case _: RuntimeException => markup_failsafe(source) }
   }
 
 }
--- a/src/Pure/Isar/isar_document.ML	Sat Jan 17 08:29:54 2009 +0100
+++ b/src/Pure/Isar/isar_document.ML	Sat Jan 17 08:30:06 2009 +0100
@@ -24,7 +24,7 @@
 type command_id = string;
 type document_id = string;
 
-fun new_id () = "isabelle:" ^ serial_string ();
+fun make_id () = "isabelle:" ^ serial_string ();
 
 fun err_dup kind id = error ("Duplicate " ^ kind ^ ": " ^ quote id);
 fun err_undef kind id = error ("Unknown " ^ kind ^ ": " ^ quote id);
@@ -53,7 +53,6 @@
 fun set_entry_state (id, state_id) = put_entry_state id (SOME state_id);
 
 
-
 (* document *)
 
 datatype document = Document of
@@ -81,11 +80,11 @@
 
 fun first_entry P (Document {start, entries, ...}) =
   let
-    fun find _ NONE = NONE
-      | find prev (SOME id) =
+    fun first _ NONE = NONE
+      | first prev (SOME id) =
           let val entry = the_entry entries id
-          in if P (id, entry) then SOME (prev, id) else find (SOME id) (#next entry) end;
-  in find NONE (SOME start) end;
+          in if P (id, entry) then SOME (prev, id, entry) else first (SOME id) (#next entry) end;
+  in first NONE (SOME start) end;
 
 
 (* modify entries *)
@@ -135,16 +134,24 @@
 end;
 
 
-fun define_state (id: state_id) state =
-  change_states (Symtab.update_new (id, state))
+(* state *)
+
+val empty_state = Future.value (SOME Toplevel.toplevel);
+
+fun define_state (id: state_id) =
+  change_states (Symtab.update_new (id, empty_state))
     handle Symtab.DUP dup => err_dup "state" dup;
 
+fun put_state (id: state_id) state = change_states (Symtab.update (id, state));
+
 fun the_state (id: state_id) =
   (case Symtab.lookup (get_states ()) id of
     NONE => err_undef "state" id
   | SOME state => state);
 
 
+(* command *)
+
 fun define_command id tr =
   change_commands (Symtab.update_new (id, Toplevel.put_id id tr))
     handle Symtab.DUP dup => err_dup "command" dup;
@@ -155,6 +162,8 @@
   | SOME tr => tr);
 
 
+(* document *)
+
 fun define_document (id: document_id) document =
   change_documents (Symtab.update_new (id, document))
     handle Symtab.DUP dup => err_dup "document" dup;
@@ -162,21 +171,38 @@
 fun the_document (id: document_id) =
   (case Symtab.lookup (get_documents ()) id of
     NONE => err_undef "document" id
-  | SOME (Document doc) => doc);
+  | SOME document => document);
+
 
 
+(** main operations **)
+
 (* begin/end document *)
 
 fun begin_document (id: document_id) path =
   let
     val (dir, name) = ThyLoad.split_thy_path path;
     val _ = define_command id Toplevel.empty;
-    val _ = define_state id (Future.value (SOME Toplevel.toplevel));
+    val _ = define_state id;
     val entries = Symtab.make [(id, make_entry NONE (SOME id))];
     val _ = define_document id (make_document dir name id entries);
   in () end;
 
-fun end_document (id: document_id) = error "FIXME";
+fun end_document (id: document_id) =
+  let
+    val document as Document {name, ...} = the_document id;
+    val end_state =
+      the_state (the (#state (#3 (the
+        (first_entry (fn (_, {next, ...}) => is_none next) document)))));
+    val _ =
+      Future.fork_deps [end_state] (fn () =>
+        (case Future.join end_state of
+          SOME st =>
+           (Toplevel.run_command name (Toplevel.put_id id (Toplevel.commit_exit Position.none)) st;
+            ThyInfo.touch_child_thys name;
+            ThyInfo.register_thy name)
+        | NONE => error ("Failed to finish theory " ^ quote name)));
+  in () end;
 
 
 (* document editing *)
@@ -185,45 +211,24 @@
 
 fun is_changed entries' (id, {next = _, state}) =
   (case try (the_entry entries') id of
-    SOME {next = _, state = state'} => state' <> state
-  | _ => true);
-
-fun cancel_state (id, {next = _, state = SOME state_id}) () = Future.cancel (the_state state_id)
-  | cancel_state _ () = ();
-
-fun update_state tr state state_id' =
-  Future.fork_deps [state] (fn () =>
-    (case Future.join state of
-      NONE => NONE
-    | SOME st => Toplevel.run_command (Toplevel.put_id state_id' tr) st));
-
-fun new_state (id, _) (state_id, updates) =
-  let
-    val state_id' = new_id ();
-    val state' = update_state (the_command id) (the_state state_id) state_id';
-    val _ = define_state state_id' state';
-  in (state_id', (id, state_id') :: updates) end;
+    NONE => true
+  | SOME {next = _, state = state'} => state' <> state);
 
-fun update_states old_document new_document =
+fun new_state name (id, _) (state_id, updates) =
   let
-    fun cancel_old id = fold_entries id cancel_state old_document ();
-
-    val Document {entries = old_entries, ...} = old_document;
-    val Document {entries = new_entries, ...} = new_document;
-  in
-    (case first_entry (is_changed old_entries) new_document of
-      NONE =>
-        (case first_entry (is_changed new_entries) old_document of
-          NONE => ([], new_document)
-        | SOME (_, id) => (cancel_old id; ([], new_document)))
-    | SOME (prev, id) =>
-        let
-          val _ = cancel_old id;
-          val prev_state_id = the (#state (the_entry new_entries (the prev)));
-          val (_, updates) = fold_entries id new_state new_document (prev_state_id, []);
-          val new_document' = new_document |> map_entries (fold set_entry_state updates);
-        in (rev updates, new_document') end)
-  end;
+    val state_id' = make_id ();
+    val _ = define_state state_id';
+    val tr = Toplevel.put_id state_id' (the_command id);
+    fun make_state' () =
+      let
+        val state = the_state state_id;
+        val state' =
+          Future.fork_deps [state] (fn () =>
+            (case Future.join state of
+              NONE => NONE
+            | SOME st => Toplevel.run_command name tr st));
+      in put_state state_id' state' end;
+  in (state_id', ((id, state_id'), make_state') :: updates) end;
 
 fun report_updates _ [] = ()
   | report_updates (document_id: document_id) updates =
@@ -233,15 +238,33 @@
 
 in
 
-fun edit_document (id: document_id) (id': document_id) edits =
+fun edit_document (old_id: document_id) (new_id: document_id) edits =
   let
-    val document = Document (the_document id);
-    val (updates, document') =
-      document
-      |> fold (fn (id, SOME id2) => insert_after id id2 | (id, NONE) => delete_after id) edits
-      |> update_states document;
-    val _ = define_document id' document';
-    val _ = report_updates id' updates;
+    val old_document as Document {name, entries = old_entries, ...} = the_document old_id;
+    val new_document as Document {entries = new_entries, ...} = old_document
+      |> fold (fn (id, SOME id2) => insert_after id id2 | (id, NONE) => delete_after id) edits;
+
+    fun cancel_old id = fold_entries id
+      (fn (_, {state = SOME state_id, ...}) => K (Future.cancel (the_state state_id)) | _ => K ())
+      old_document ();
+
+    val (updates, new_document') =
+      (case first_entry (is_changed old_entries) new_document of
+        NONE =>
+          (case first_entry (is_changed new_entries) old_document of
+            NONE => ([], new_document)
+          | SOME (_, id, _) => (cancel_old id; ([], new_document)))
+      | SOME (prev, id, _) =>
+          let
+            val _ = cancel_old id;
+            val prev_state_id = the (#state (the_entry new_entries (the prev)));
+            val (_, updates) = fold_entries id (new_state name) new_document (prev_state_id, []);
+            val new_document' = new_document |> map_entries (fold (set_entry_state o #1) updates);
+          in (rev updates, new_document') end);
+
+    val _ = define_document new_id new_document';
+    val _ = report_updates new_id (map #1 updates);
+    val _ = List.app (fn (_, run) => run ()) updates;
   in () end;
 
 end;
--- a/src/Pure/Isar/toplevel.ML	Sat Jan 17 08:29:54 2009 +0100
+++ b/src/Pure/Isar/toplevel.ML	Sat Jan 17 08:30:06 2009 +0100
@@ -96,7 +96,7 @@
   val transition: bool -> transition -> state -> (state * (exn * string) option) option
   val commit_exit: Position.T -> transition
   val command: transition -> state -> state
-  val run_command: transition -> state -> state option
+  val run_command: string -> transition -> state -> state option
   val excursion: (transition * transition list) list -> (transition * state) list lazy
 end;
 
@@ -698,11 +698,17 @@
   let val st' = command tr st
   in (st', st') end;
 
-fun run_command tr st =
-  (case transition true tr st of
-    SOME (st', NONE) => (status tr Markup.finished; SOME st')
-  | SOME (_, SOME exn_info) => (error_msg tr exn_info; status tr Markup.failed; NONE)
-  | NONE => (error_msg tr (TERMINATE, at_command tr); status tr Markup.failed; NONE));
+fun run_command thy_name tr st =
+  (case
+      (case init_of tr of
+        SOME name => Exn.capture (fn () => ThyLoad.check_name thy_name name) ()
+      | NONE => Exn.Result ()) of
+    Exn.Result () =>
+      (case transition true tr st of
+        SOME (st', NONE) => (status tr Markup.finished; SOME st')
+      | SOME (_, SOME exn_info) => (error_msg tr exn_info; status tr Markup.failed; NONE)
+      | NONE => (error_msg tr (TERMINATE, at_command tr); status tr Markup.failed; NONE))
+  | Exn.Exn exn => (error_msg tr (exn, at_command tr); status tr Markup.failed; NONE));
 
 
 (* excursion of units, consisting of commands with proof *)
--- a/src/Pure/Thy/thy_load.ML	Sat Jan 17 08:29:54 2009 +0100
+++ b/src/Pure/Thy/thy_load.ML	Sat Jan 17 08:30:06 2009 +0100
@@ -25,6 +25,7 @@
   val check_file: Path.T -> Path.T -> (Path.T * File.ident) option
   val check_ml: Path.T -> Path.T -> (Path.T * File.ident) option
   val check_thy: Path.T -> string -> Path.T * File.ident
+  val check_name: string -> string -> unit
   val deps_thy: Path.T -> string ->
    {master: Path.T * File.ident, text: string list, imports: string list, uses: Path.T list}
   val load_ml: Path.T -> Path.T -> Path.T * File.ident
@@ -95,6 +96,11 @@
     | SOME thy_id => thy_id)
   end;
 
+fun check_name name name' =
+  if name = name' then ()
+  else error ("Filename " ^ quote (Path.implode (thy_path name)) ^
+    " does not agree with theory name " ^ quote name');
+
 
 (* theory deps *)
 
@@ -104,9 +110,7 @@
     val text = explode (File.read path);
     val (name', imports, uses) =
       ThyHeader.read (Path.position path) (Source.of_list_limited 8000 text);
-    val _ = name = name' orelse
-      error ("Filename " ^ quote (Path.implode (Path.base path)) ^
-        " does not agree with theory name " ^ quote name');
+    val _ = check_name name name';
     val uses = map (Path.explode o #1) uses;
   in {master = master, text = text, imports = imports, uses = uses} end;
 
--- a/src/Pure/Tools/isabelle_process.ML	Sat Jan 17 08:29:54 2009 +0100
+++ b/src/Pure/Tools/isabelle_process.ML	Sat Jan 17 08:30:06 2009 +0100
@@ -55,9 +55,6 @@
   let val clean = clean_string [Symbol.STX, "\n", "\r"]
   in implode (map (fn (x, y) => clean x ^ "=" ^ clean y ^ special_sep ^ "\n") props) end;
 
-fun message_text class body =
-  YXML.element Markup.messageN [(Markup.classN, class)] [clean_string [Symbol.STX] body];
-
 fun message_pos trees = trees |> get_first
   (fn XML.Elem (name, atts, ts) =>
         if name = Markup.positionN then SOME (Position.of_properties atts)
@@ -69,21 +66,21 @@
 
 in
 
-fun message _ _ _ "" = ()
-  | message out_stream ch class body =
+fun message _ _ "" = ()
+  | message out_stream ch body =
       let
         val pos = the_default Position.none (message_pos (YXML.parse_body body));
         val props =
           Position.properties_of (Position.thread_data ())
           |> Position.default_properties pos;
-        val txt = message_text class body;
+        val txt = clean_string [Symbol.STX] body;
       in output out_stream (special ch ^ message_props props ^ txt ^ special_end) end;
 
 fun init_message out_stream =
   let
     val pid = (Markup.pidN, process_id ());
     val session = (Markup.sessionN, List.last (Session.id ()) handle List.Empty => "unknown");
-    val text = message_text Markup.initN (Session.welcome ());
+    val text = Session.welcome ();
   in output out_stream (special "A" ^ message_props [pid, session] ^ text ^ special_end) end;
 
 end;
@@ -116,13 +113,13 @@
     val _ = SimpleThread.fork false (auto_flush out_stream);
     val _ = SimpleThread.fork false (auto_flush TextIO.stdErr);
   in
-    Output.status_fn   := message out_stream "B" Markup.statusN;
-    Output.writeln_fn  := message out_stream "C" Markup.writelnN;
-    Output.priority_fn := message out_stream "D" Markup.priorityN;
-    Output.tracing_fn  := message out_stream "E" Markup.tracingN;
-    Output.warning_fn  := message out_stream "F" Markup.warningN;
-    Output.error_fn    := message out_stream "G" Markup.errorN;
-    Output.debug_fn    := message out_stream "H" Markup.debugN;
+    Output.status_fn   := message out_stream "B";
+    Output.writeln_fn  := message out_stream "C";
+    Output.priority_fn := message out_stream "D";
+    Output.tracing_fn  := message out_stream "E";
+    Output.warning_fn  := message out_stream "F";
+    Output.error_fn    := message out_stream "G";
+    Output.debug_fn    := message out_stream "H";
     Output.prompt_fn   := ignore;
     out_stream
   end;
--- a/src/Pure/Tools/isabelle_process.scala	Sat Jan 17 08:29:54 2009 +0100
+++ b/src/Pure/Tools/isabelle_process.scala	Sat Jan 17 08:30:06 2009 +0100
@@ -50,6 +50,21 @@
       ('2' : Int) -> Kind.STDOUT,
       ('3' : Int) -> Kind.SIGNAL,
       ('4' : Int) -> Kind.EXIT)
+    // message markup
+    val markup = Map(
+      Kind.INIT -> Markup.INIT,
+      Kind.STATUS -> Markup.STATUS,
+      Kind.WRITELN -> Markup.WRITELN,
+      Kind.PRIORITY -> Markup.PRIORITY,
+      Kind.TRACING -> Markup.TRACING,
+      Kind.WARNING -> Markup.WARNING,
+      Kind.ERROR -> Markup.ERROR,
+      Kind.DEBUG -> Markup.DEBUG,
+      Kind.SYSTEM -> Markup.SYSTEM,
+      Kind.STDIN -> Markup.STDIN,
+      Kind.STDOUT -> Markup.STDOUT,
+      Kind.SIGNAL -> Markup.SIGNAL,
+      Kind.EXIT -> Markup.EXIT)
     //}}}
     def is_raw(kind: Value) =
       kind == STDOUT
@@ -67,8 +82,10 @@
 
   class Result(val kind: Kind.Value, val props: Properties, val result: String) {
     override def toString = {
-      val tree = YXML.parse_failsafe(result)
-      val res = if (kind == Kind.STATUS) tree.toString else XML.content(tree).mkString
+      val trees = YXML.parse_body_failsafe(result)
+      val res =
+        if (kind == Kind.STATUS) trees.map(_.toString).mkString
+        else trees.flatMap(XML.content(_).mkString).mkString
       if (props == null) kind.toString + " [[" + res + "]]"
       else kind.toString + " " + props.toString + " [[" + res + "]]"
     }
@@ -77,6 +94,10 @@
     def is_system = Kind.is_system(kind)
   }
 
+  def parse_message(kind: Kind.Value, result: String) = {
+    XML.Elem(Markup.MESSAGE, List((Markup.CLASS, Kind.markup(kind))),
+      YXML.parse_body_failsafe(result))
+  }
 }