--- 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))
+ }
}