# HG changeset patch # User wenzelm # Date 1232115706 -3600 # Node ID c3b9c0d24fecbf7eabb069c683c6cd290fedec97 # Parent fc20414d4aa8bea5e20e71c4b3eb7b5d95c3c4f4# Parent d7648f30f923ba9cb8377aa533c2ca7f9d4ac1e3 merged diff -r fc20414d4aa8 -r c3b9c0d24fec src/Pure/Isar/isar_document.ML --- 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 diff -r fc20414d4aa8 -r c3b9c0d24fec src/Pure/Isar/toplevel.ML --- 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 *) diff -r fc20414d4aa8 -r c3b9c0d24fec src/Pure/Thy/thy_load.ML --- 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;