get theory from last executation state;
authorwenzelm
Tue Jul 05 20:36:49 2011 +0200 (2011-07-05)
changeset 43668aad4f1956098
parent 43667 6d73cceb1503
child 43669 9d34288e9351
get theory from last executation state;
tuned error messages;
src/Pure/Isar/toplevel.ML
src/Pure/PIDE/document.ML
src/Pure/PIDE/isar_document.ML
     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,15 +50,23 @@
    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 -val empty_version = Version Graph.empty;
    2.24 +fun make_node (last, entries) =
    2.25 +  Node {last = last, entries = entries};
    2.26 +
    2.27 +fun get_last (Node {last, ...}) = last;
    2.28 +fun set_last last (Node {entries, ...}) = make_node (last, entries);
    2.29  
    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 +fun map_entries f (Node {last, entries}) = make_node (last, f entries);
    2.33 +fun fold_entries start f (Node {entries, ...}) = Entries.fold start f entries;
    2.34 +fun first_entry start P (Node {entries, ...}) = Entries.get_first start P entries;
    2.35 +
    2.36 +val empty_node = make_node (no_id, Entries.empty);
    2.37 +val empty_version = Version Graph.empty;
    2.38  
    2.39  
    2.40  (* node edits and associated executions *)
    2.41 @@ -67,23 +76,22 @@
    2.42    (*NONE: remove node, SOME: insert/remove commands*)
    2.43    ((command_id option * command_id option) list) option;
    2.44  
    2.45 -fun the_entry (Node entries) id =
    2.46 +fun the_entry (Node {entries, ...}) id =
    2.47    (case Entries.lookup entries id of
    2.48      NONE => err_undef "command entry" id
    2.49    | SOME entry => entry);
    2.50  
    2.51 -fun update_entry (id, exec_id) (Node entries) =
    2.52 -  Node (Entries.update (id, SOME exec_id) entries);
    2.53 +fun update_entry (id, exec_id) =
    2.54 +  map_entries (Entries.update (id, SOME exec_id));
    2.55  
    2.56  fun reset_after id entries =
    2.57    (case Entries.get_after entries id of
    2.58      NONE => entries
    2.59    | SOME next => Entries.update (next, NONE) entries);
    2.60  
    2.61 -fun edit_node (id, SOME id2) (Node entries) =
    2.62 -      Node (Entries.insert_after id (id2, NONE) entries)
    2.63 -  | edit_node (id, NONE) (Node entries) =
    2.64 -      Node (entries |> Entries.delete_after id |> reset_after id);
    2.65 +val edit_node = map_entries o fold
    2.66 +  (fn (id, SOME id2) => Entries.insert_after id (id2, NONE)
    2.67 +    | (id, NONE) => Entries.delete_after id #> reset_after id);
    2.68  
    2.69  
    2.70  (* version operations *)
    2.71 @@ -97,7 +105,7 @@
    2.72  fun edit_nodes (name, SOME edits) (Version nodes) =
    2.73        Version (nodes
    2.74          |> Graph.default_node (name, empty_node)
    2.75 -        |> Graph.map_node name (fold edit_node edits))
    2.76 +        |> Graph.map_node name (edit_node edits))
    2.77    | edit_nodes (name, NONE) (Version nodes) =
    2.78        Version (perhaps (try (Graph.del_node name)) nodes);
    2.79  
    2.80 @@ -182,6 +190,12 @@
    2.81      NONE => err_undef "command execution" id
    2.82    | SOME exec => exec);
    2.83  
    2.84 +fun get_theory state version_id pos name =
    2.85 +  let
    2.86 +    val last = get_last (get_node (the_version state version_id) name);
    2.87 +    val st = #2 (Lazy.force (the_exec state last));
    2.88 +  in Toplevel.end_theory pos st end;
    2.89 +
    2.90  
    2.91  (* document execution *)
    2.92  
    2.93 @@ -309,9 +323,9 @@
    2.94                  (case prev of
    2.95                    NONE => no_id
    2.96                  | SOME prev_id => the_default no_id (the_entry node prev_id));
    2.97 -              val (_, rev_upds, st') =
    2.98 +              val (last, rev_upds, st') =
    2.99                  fold_entries (SOME id) (new_exec name o #2 o #1) node (prev_exec, [], st);
   2.100 -              val node' = fold update_entry rev_upds node;
   2.101 +              val node' = node |> fold update_entry rev_upds |> set_last last;
   2.102              in (rev_upds @ rev_updates, put_node name node' version, st') end)
   2.103        end;
   2.104  
     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));