removed slightly odd Isar_Document.init;
authorwenzelm
Tue Dec 29 20:30:40 2009 +0100 (2009-12-29 ago)
changeset 34206c29264a16ad8
parent 34205 f69cd974bc4e
child 34207 88300168baf8
removed slightly odd Isar_Document.init;
simplified begin_document: associate empty command/state with no_id, which is implicit start;
replaced make_id by create_id (cf. Scala version);
eliminated CRITICAL/Unsynchronized.ref in favour of Synchronized.var;
tuned;
src/Pure/Isar/isar_document.ML
src/Pure/System/isabelle_process.ML
     1.1 --- a/src/Pure/Isar/isar_document.ML	Tue Dec 29 16:20:39 2009 +0100
     1.2 +++ b/src/Pure/Isar/isar_document.ML	Tue Dec 29 20:30:40 2009 +0100
     1.3 @@ -9,11 +9,12 @@
     1.4    type state_id = string
     1.5    type command_id = string
     1.6    type document_id = string
     1.7 +  val no_id: string
     1.8 +  val create_id: unit -> string
     1.9    val define_command: command_id -> Toplevel.transition -> unit
    1.10    val begin_document: document_id -> Path.T -> unit
    1.11    val end_document: document_id -> unit
    1.12    val edit_document: document_id -> document_id -> (command_id * command_id option) list -> unit
    1.13 -  val init: unit -> unit
    1.14  end;
    1.15  
    1.16  structure Isar_Document: ISAR_DOCUMENT =
    1.17 @@ -25,10 +26,20 @@
    1.18  type command_id = string;
    1.19  type document_id = string;
    1.20  
    1.21 -fun make_id () = "i" ^ serial_string ();
    1.22 +val no_id = "";
    1.23 +
    1.24 +local
    1.25 +  val id_count = Synchronized.var "id" 0;
    1.26 +in
    1.27 +  fun create_id () =
    1.28 +    Synchronized.change_result id_count
    1.29 +      (fn i =>
    1.30 +        let val i' = i + 1
    1.31 +        in ("i" ^ string_of_int i', i') end);
    1.32 +end;
    1.33  
    1.34  fun err_dup kind id = error ("Duplicate " ^ kind ^ ": " ^ quote id);
    1.35 -fun err_undef kind id = error ("Unknown " ^ kind ^ ": " ^ quote id);
    1.36 +fun err_undef kind id = error ("Undefined " ^ kind ^ ": " ^ quote id);
    1.37  
    1.38  
    1.39  
    1.40 @@ -57,16 +68,15 @@
    1.41  (* document *)
    1.42  
    1.43  datatype document = Document of
    1.44 - {dir: Path.T,                    (*master directory*)
    1.45 -  name: string,                   (*theory name*)
    1.46 -  start: command_id,              (*empty start command*)
    1.47 -  entries: entry Symtab.table};   (*unique command entries indexed by command_id*)
    1.48 + {dir: Path.T,                   (*master directory*)
    1.49 +  name: string,                  (*theory name*)
    1.50 +  entries: entry Symtab.table};  (*unique command entries indexed by command_id, start with no_id*)
    1.51  
    1.52 -fun make_document dir name start entries =
    1.53 -  Document {dir = dir, name = name, start = start, entries = entries};
    1.54 +fun make_document dir name entries =
    1.55 +  Document {dir = dir, name = name, entries = entries};
    1.56  
    1.57 -fun map_entries f (Document {dir, name, start, entries}) =
    1.58 -  make_document dir name start (f entries);
    1.59 +fun map_entries f (Document {dir, name, entries}) =
    1.60 +  make_document dir name (f entries);
    1.61  
    1.62  
    1.63  (* iterate entries *)
    1.64 @@ -79,13 +89,13 @@
    1.65            in apply (#next entry) (f (id, entry) x) end;
    1.66    in if Symtab.defined entries id0 then apply (SOME id0) else I end;
    1.67  
    1.68 -fun first_entry P (Document {start, entries, ...}) =
    1.69 +fun first_entry P (Document {entries, ...}) =
    1.70    let
    1.71      fun first _ NONE = NONE
    1.72        | first prev (SOME id) =
    1.73            let val entry = the_entry entries id
    1.74            in if P (id, entry) then SOME (prev, id, entry) else first (SOME id) (#next entry) end;
    1.75 -  in first NONE (SOME start) end;
    1.76 +  in first NONE (SOME no_id) end;
    1.77  
    1.78  
    1.79  (* modify entries *)
    1.80 @@ -112,81 +122,85 @@
    1.81  
    1.82  (** global configuration **)
    1.83  
    1.84 +(* states *)
    1.85 +
    1.86 +val empty_state = Future.value (SOME Toplevel.toplevel);
    1.87 +
    1.88  local
    1.89 -  val global_states = Unsynchronized.ref (Symtab.empty: Toplevel.state option future Symtab.table);
    1.90 -  val global_commands = Unsynchronized.ref (Symtab.empty: Toplevel.transition Symtab.table);
    1.91 -  val global_documents = Unsynchronized.ref (Symtab.empty: document Symtab.table);
    1.92 +
    1.93 +val global_states =
    1.94 +  Synchronized.var "global_states" (Symtab.make [(no_id, empty_state)]);
    1.95 +
    1.96  in
    1.97  
    1.98 -fun change_states f = NAMED_CRITICAL "Isar" (fn () => Unsynchronized.change global_states f);
    1.99 -fun get_states () = ! global_states;
   1.100 -
   1.101 -fun change_commands f = NAMED_CRITICAL "Isar" (fn () => Unsynchronized.change global_commands f);
   1.102 -fun get_commands () = ! global_commands;
   1.103 +fun define_state (id: state_id) =
   1.104 +  Synchronized.change global_states (Symtab.update_new (id, empty_state))
   1.105 +    handle Symtab.DUP dup => err_dup "state" dup;
   1.106  
   1.107 -fun change_documents f = NAMED_CRITICAL "Isar" (fn () => Unsynchronized.change global_documents f);
   1.108 -fun get_documents () = ! global_documents;
   1.109 +fun put_state (id: state_id) state =
   1.110 +  Synchronized.change global_states (Symtab.update (id, state));
   1.111  
   1.112 -fun init () = NAMED_CRITICAL "Isar" (fn () =>
   1.113 - (global_states := Symtab.empty;
   1.114 -  global_commands := Symtab.empty;
   1.115 -  global_documents := Symtab.empty));
   1.116 +fun the_state (id: state_id) =
   1.117 +  (case Symtab.lookup (Synchronized.value global_states) id of
   1.118 +    NONE => err_undef "state" id
   1.119 +  | SOME state => state);
   1.120  
   1.121  end;
   1.122  
   1.123  
   1.124 -(* state *)
   1.125 -
   1.126 -val empty_state = Future.value (SOME Toplevel.toplevel);
   1.127 +(* commands *)
   1.128  
   1.129 -fun define_state (id: state_id) =
   1.130 -  change_states (Symtab.update_new (id, empty_state))
   1.131 -    handle Symtab.DUP dup => err_dup "state" dup;
   1.132 +local
   1.133  
   1.134 -fun put_state (id: state_id) state = change_states (Symtab.update (id, state));
   1.135 +val global_commands =
   1.136 +  Synchronized.var "global_commands" (Symtab.make [(no_id, Toplevel.empty)]);
   1.137  
   1.138 -fun the_state (id: state_id) =
   1.139 -  (case Symtab.lookup (get_states ()) id of
   1.140 -    NONE => err_undef "state" id
   1.141 -  | SOME state => state);
   1.142 -
   1.143 -
   1.144 -(* command *)
   1.145 +in
   1.146  
   1.147  fun define_command id tr =
   1.148 -  change_commands (Symtab.update_new (id, Toplevel.put_id id tr))
   1.149 +  Synchronized.change global_commands (Symtab.update_new (id, Toplevel.put_id id tr))
   1.150      handle Symtab.DUP dup => err_dup "command" dup;
   1.151  
   1.152  fun the_command (id: command_id) =
   1.153 -  (case Symtab.lookup (get_commands ()) id of
   1.154 +  (case Symtab.lookup (Synchronized.value global_commands) id of
   1.155      NONE => err_undef "command" id
   1.156    | SOME tr => tr);
   1.157  
   1.158 +end;
   1.159  
   1.160 -(* document *)
   1.161 +
   1.162 +(* documents *)
   1.163 +
   1.164 +local
   1.165 +
   1.166 +val global_documents =
   1.167 +  Synchronized.var "global_documents" (Symtab.empty: document Symtab.table);
   1.168 +
   1.169 +in
   1.170  
   1.171  fun define_document (id: document_id) document =
   1.172 -  change_documents (Symtab.update_new (id, document))
   1.173 +  Synchronized.change global_documents (Symtab.update_new (id, document))
   1.174      handle Symtab.DUP dup => err_dup "document" dup;
   1.175  
   1.176  fun the_document (id: document_id) =
   1.177 -  (case Symtab.lookup (get_documents ()) id of
   1.178 +  (case Symtab.lookup (Synchronized.value global_documents) id of
   1.179      NONE => err_undef "document" id
   1.180    | SOME document => document);
   1.181  
   1.182 +end;
   1.183 +
   1.184  
   1.185  
   1.186  (** main operations **)
   1.187  
   1.188  (* begin/end document *)
   1.189  
   1.190 +val no_entries = Symtab.make [(no_id, make_entry NONE (SOME no_id))];
   1.191 +
   1.192  fun begin_document (id: document_id) path =
   1.193    let
   1.194      val (dir, name) = ThyLoad.split_thy_path path;
   1.195 -    val _ = define_command id Toplevel.empty;
   1.196 -    val _ = define_state id;
   1.197 -    val entries = Symtab.make [(id, make_entry NONE (SOME id))];
   1.198 -    val _ = define_document id (make_document dir name id entries);
   1.199 +    val _ = define_document id (make_document dir name no_entries);
   1.200    in () end;
   1.201  
   1.202  fun end_document (id: document_id) =
   1.203 @@ -217,7 +231,7 @@
   1.204  
   1.205  fun new_state name (id, _) (state_id, updates) =
   1.206    let
   1.207 -    val state_id' = make_id ();
   1.208 +    val state_id' = create_id ();
   1.209      val _ = define_state state_id';
   1.210      val tr = Toplevel.put_id state_id' (the_command id);
   1.211      fun make_state' () =
     2.1 --- a/src/Pure/System/isabelle_process.ML	Tue Dec 29 16:20:39 2009 +0100
     2.2 +++ b/src/Pure/System/isabelle_process.ML	Tue Dec 29 20:30:40 2009 +0100
     2.3 @@ -95,7 +95,6 @@
     2.4   (Unsynchronized.change print_mode (update (op =) isabelle_processN);
     2.5    setup_channels out |> init_message;
     2.6    OuterKeyword.report ();
     2.7 -  Isar_Document.init ();
     2.8    Output.status (Markup.markup Markup.ready "");
     2.9    Isar.toplevel_loop {init = true, welcome = false, sync = true, secure = true});
    2.10