--- a/src/Pure/Isar/isar_document.ML Fri Jan 16 15:19:10 2009 +0100
+++ b/src/Pure/Isar/isar_document.ML Fri Jan 16 15:21:46 2009 +0100
@@ -81,11 +81,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) else first (SOME id) (#next entry) end;
+ in first NONE (SOME start) end;
(* modify entries *)
@@ -162,7 +162,7 @@
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);
(* begin/end document *)
@@ -185,31 +185,30 @@
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 _ () = ();
+ NONE => true
+ | SOME {next = _, state = state'} => state' <> 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) =
+fun new_state name (id, _) (state_id, updates) =
let
val state_id' = new_id ();
- val state' = update_state (the_command id) (the_state state_id) state_id';
+ val tr = Toplevel.put_id state_id' (the_command id);
+ 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));
val _ = define_state state_id' state';
in (state_id', (id, state_id') :: updates) end;
fun update_states old_document new_document =
let
- fun cancel_old id = fold_entries id cancel_state old_document ();
+ fun cancel_old id = fold_entries id
+ (fn (_, {state = SOME state_id, ...}) => K (Future.cancel (the_state state_id)) | _ => K ())
+ old_document ();
val Document {entries = old_entries, ...} = old_document;
- val Document {entries = new_entries, ...} = new_document;
+ val Document {name, entries = new_entries, ...} = new_document;
in
(case first_entry (is_changed old_entries) new_document of
NONE =>
@@ -220,7 +219,7 @@
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 (_, updates) = fold_entries id (new_state name) new_document (prev_state_id, []);
val new_document' = new_document |> map_entries (fold set_entry_state updates);
in (rev updates, new_document') end)
end;
@@ -235,7 +234,7 @@
fun edit_document (id: document_id) (id': document_id) edits =
let
- val document = Document (the_document id);
+ val document = the_document id;
val (updates, document') =
document
|> fold (fn (id, SOME id2) => insert_after id id2 | (id, NONE) => delete_after id) edits
--- a/src/Pure/Isar/toplevel.ML Fri Jan 16 15:19:10 2009 +0100
+++ b/src/Pure/Isar/toplevel.ML Fri Jan 16 15:21:46 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 Fri Jan 16 15:19:10 2009 +0100
+++ b/src/Pure/Thy/thy_load.ML Fri Jan 16 15:21:46 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;