1.1 --- a/src/Pure/Isar/toplevel.ML Tue Jul 05 19:45:59 2011 +0200
1.2 +++ b/src/Pure/Isar/toplevel.ML Tue Jul 05 20:36:49 2011 +0200
1.3 @@ -186,7 +186,8 @@
1.4 | _ => raise UNDEF);
1.5
1.6 fun end_theory _ (State (NONE, SOME (Theory (Context.Theory thy, _)))) = thy
1.7 - | end_theory pos _ = error ("Unfinished theory at end of input" ^ Position.str_of pos);
1.8 + | end_theory pos (State (SOME _, _)) = error ("Unfinished theory " ^ Position.str_of pos)
1.9 + | end_theory pos (State (NONE, NONE)) = error ("Missing theory " ^ Position.str_of pos);
1.10
1.11
1.12 (* print state *)
2.1 --- a/src/Pure/PIDE/document.ML Tue Jul 05 19:45:59 2011 +0200
2.2 +++ b/src/Pure/PIDE/document.ML Tue Jul 05 20:36:49 2011 +0200
2.3 @@ -18,6 +18,7 @@
2.4 type edit = string * ((command_id option * command_id option) list) option
2.5 type state
2.6 val init_state: state
2.7 + val get_theory: state -> version_id -> Position.T -> string -> theory
2.8 val cancel_execution: state -> unit -> unit
2.9 val define_command: command_id -> string -> state -> state
2.10 val edit: version_id -> version_id -> edit list -> state -> (command_id * exec_id) list * state
2.11 @@ -49,16 +50,24 @@
2.12
2.13 structure Entries = Linear_Set(type key = command_id val ord = int_ord);
2.14
2.15 -abstype node = Node of exec_id option Entries.T (*command entries with excecutions*)
2.16 - and version = Version of node Graph.T (*development graph wrt. static imports*)
2.17 +abstype node = Node of
2.18 + {last: exec_id, entries: exec_id option Entries.T} (*command entries with excecutions*)
2.19 +and version = Version of node Graph.T (*development graph wrt. static imports*)
2.20 with
2.21
2.22 -val empty_node = Node Entries.empty;
2.23 +fun make_node (last, entries) =
2.24 + Node {last = last, entries = entries};
2.25 +
2.26 +fun get_last (Node {last, ...}) = last;
2.27 +fun set_last last (Node {entries, ...}) = make_node (last, entries);
2.28 +
2.29 +fun map_entries f (Node {last, entries}) = make_node (last, f entries);
2.30 +fun fold_entries start f (Node {entries, ...}) = Entries.fold start f entries;
2.31 +fun first_entry start P (Node {entries, ...}) = Entries.get_first start P entries;
2.32 +
2.33 +val empty_node = make_node (no_id, Entries.empty);
2.34 val empty_version = Version Graph.empty;
2.35
2.36 -fun fold_entries start f (Node entries) = Entries.fold start f entries;
2.37 -fun first_entry start P (Node entries) = Entries.get_first start P entries;
2.38 -
2.39
2.40 (* node edits and associated executions *)
2.41
2.42 @@ -67,23 +76,22 @@
2.43 (*NONE: remove node, SOME: insert/remove commands*)
2.44 ((command_id option * command_id option) list) option;
2.45
2.46 -fun the_entry (Node entries) id =
2.47 +fun the_entry (Node {entries, ...}) id =
2.48 (case Entries.lookup entries id of
2.49 NONE => err_undef "command entry" id
2.50 | SOME entry => entry);
2.51
2.52 -fun update_entry (id, exec_id) (Node entries) =
2.53 - Node (Entries.update (id, SOME exec_id) entries);
2.54 +fun update_entry (id, exec_id) =
2.55 + map_entries (Entries.update (id, SOME exec_id));
2.56
2.57 fun reset_after id entries =
2.58 (case Entries.get_after entries id of
2.59 NONE => entries
2.60 | SOME next => Entries.update (next, NONE) entries);
2.61
2.62 -fun edit_node (id, SOME id2) (Node entries) =
2.63 - Node (Entries.insert_after id (id2, NONE) entries)
2.64 - | edit_node (id, NONE) (Node entries) =
2.65 - Node (entries |> Entries.delete_after id |> reset_after id);
2.66 +val edit_node = map_entries o fold
2.67 + (fn (id, SOME id2) => Entries.insert_after id (id2, NONE)
2.68 + | (id, NONE) => Entries.delete_after id #> reset_after id);
2.69
2.70
2.71 (* version operations *)
2.72 @@ -97,7 +105,7 @@
2.73 fun edit_nodes (name, SOME edits) (Version nodes) =
2.74 Version (nodes
2.75 |> Graph.default_node (name, empty_node)
2.76 - |> Graph.map_node name (fold edit_node edits))
2.77 + |> Graph.map_node name (edit_node edits))
2.78 | edit_nodes (name, NONE) (Version nodes) =
2.79 Version (perhaps (try (Graph.del_node name)) nodes);
2.80
2.81 @@ -182,6 +190,12 @@
2.82 NONE => err_undef "command execution" id
2.83 | SOME exec => exec);
2.84
2.85 +fun get_theory state version_id pos name =
2.86 + let
2.87 + val last = get_last (get_node (the_version state version_id) name);
2.88 + val st = #2 (Lazy.force (the_exec state last));
2.89 + in Toplevel.end_theory pos st end;
2.90 +
2.91
2.92 (* document execution *)
2.93
2.94 @@ -309,9 +323,9 @@
2.95 (case prev of
2.96 NONE => no_id
2.97 | SOME prev_id => the_default no_id (the_entry node prev_id));
2.98 - val (_, rev_upds, st') =
2.99 + val (last, rev_upds, st') =
2.100 fold_entries (SOME id) (new_exec name o #2 o #1) node (prev_exec, [], st);
2.101 - val node' = fold update_entry rev_upds node;
2.102 + val node' = node |> fold update_entry rev_upds |> set_last last;
2.103 in (rev_upds @ rev_updates, put_node name node' version, st') end)
2.104 end;
2.105
3.1 --- a/src/Pure/PIDE/isar_document.ML Tue Jul 05 19:45:59 2011 +0200
3.2 +++ b/src/Pure/PIDE/isar_document.ML Tue Jul 05 20:36:49 2011 +0200
3.3 @@ -4,12 +4,19 @@
3.4 Protocol message formats for interactive Isar documents.
3.5 *)
3.6
3.7 -structure Isar_Document: sig end =
3.8 +signature ISAR_DOCUMENT =
3.9 +sig
3.10 + val state: unit -> Document.state
3.11 +end
3.12 +
3.13 +structure Isar_Document: ISAR_DOCUMENT =
3.14 struct
3.15
3.16 val global_state = Synchronized.var "Isar_Document" Document.init_state;
3.17 val change_state = Synchronized.change global_state;
3.18
3.19 +fun state () = Synchronized.value global_state;
3.20 +
3.21 val _ =
3.22 Isabelle_Process.add_command "Isar_Document.define_command"
3.23 (fn [id, text] => change_state (Document.define_command (Document.parse_id id) text));