src/Pure/Isar/isar_document.ML
changeset 38355 8cb265fb12fe
parent 38271 36187e8443dd
child 38363 af7f41a8a0a8
     1.1 --- a/src/Pure/Isar/isar_document.ML	Wed Aug 11 18:44:06 2010 +0200
     1.2 +++ b/src/Pure/Isar/isar_document.ML	Wed Aug 11 22:41:26 2010 +0200
     1.3 @@ -20,18 +20,17 @@
     1.4      Synchronized.change_result id_count
     1.5        (fn i =>
     1.6          let val i' = i + 1
     1.7 -        in ("i" ^ string_of_int i', i') end);
     1.8 +        in (i', i') end);
     1.9  end;
    1.10  
    1.11 -fun err_dup kind id = error ("Duplicate " ^ kind ^ ": " ^ quote id);
    1.12 -fun err_undef kind id = error ("Undefined " ^ kind ^ ": " ^ quote id);
    1.13 -
    1.14 +fun err_dup kind id = error ("Duplicate " ^ kind ^ ": " ^ Document.print_id id);
    1.15 +fun err_undef kind id = error ("Undefined " ^ kind ^ ": " ^ Document.print_id id);
    1.16  
    1.17  
    1.18  (** documents **)
    1.19  
    1.20  datatype entry = Entry of {next: Document.command_id option, state: Document.state_id option};
    1.21 -type node = entry Symtab.table; (*unique command entries indexed by command_id, start with no_id*)
    1.22 +type node = entry Inttab.table; (*unique command entries indexed by command_id, start with no_id*)
    1.23  type document = node Graph.T;   (*development graph via static imports*)
    1.24  
    1.25  
    1.26 @@ -40,11 +39,11 @@
    1.27  fun make_entry next state = Entry {next = next, state = state};
    1.28  
    1.29  fun the_entry (node: node) (id: Document.command_id) =
    1.30 -  (case Symtab.lookup node id of
    1.31 +  (case Inttab.lookup node id of
    1.32      NONE => err_undef "command entry" id
    1.33    | SOME (Entry entry) => entry);
    1.34  
    1.35 -fun put_entry (id: Document.command_id, entry: entry) = Symtab.update (id, entry);
    1.36 +fun put_entry (id: Document.command_id, entry: entry) = Inttab.update (id, entry);
    1.37  
    1.38  fun put_entry_state (id: Document.command_id) state (node: node) =
    1.39    let val {next, ...} = the_entry node id
    1.40 @@ -62,7 +61,7 @@
    1.41        | apply (SOME id) x =
    1.42            let val entry = the_entry node id
    1.43            in apply (#next entry) (f (id, entry) x) end;
    1.44 -  in if Symtab.defined node id0 then apply (SOME id0) else I end;
    1.45 +  in if Inttab.defined node id0 then apply (SOME id0) else I end;
    1.46  
    1.47  fun first_entry P (node: node) =
    1.48    let
    1.49 @@ -85,7 +84,7 @@
    1.50  fun delete_after (id: Document.command_id) (node: node) =
    1.51    let val {next, state} = the_entry node id in
    1.52      (case next of
    1.53 -      NONE => error ("No next entry to delete: " ^ quote id)
    1.54 +      NONE => error ("No next entry to delete: " ^ Document.print_id id)
    1.55      | SOME id2 =>
    1.56          node |>
    1.57            (case #next (the_entry node id2) of
    1.58 @@ -96,7 +95,7 @@
    1.59  
    1.60  (* node operations *)
    1.61  
    1.62 -val empty_node: node = Symtab.make [(Document.no_id, make_entry NONE (SOME Document.no_id))];
    1.63 +val empty_node: node = Inttab.make [(Document.no_id, make_entry NONE (SOME Document.no_id))];
    1.64  
    1.65  fun the_node (document: document) name =
    1.66    Graph.get_node document name handle Graph.UNDEF _ => empty_node;
    1.67 @@ -118,17 +117,17 @@
    1.68  local
    1.69  
    1.70  val global_states =
    1.71 -  Unsynchronized.ref (Symtab.make [(Document.no_id, Lazy.value (SOME Toplevel.toplevel))]);
    1.72 +  Unsynchronized.ref (Inttab.make [(Document.no_id, Lazy.value (SOME Toplevel.toplevel))]);
    1.73  
    1.74  in
    1.75  
    1.76  fun define_state (id: Document.state_id) state =
    1.77    NAMED_CRITICAL "Isar" (fn () =>
    1.78 -    Unsynchronized.change global_states (Symtab.update_new (id, state))
    1.79 -      handle Symtab.DUP dup => err_dup "state" dup);
    1.80 +    Unsynchronized.change global_states (Inttab.update_new (id, state))
    1.81 +      handle Inttab.DUP dup => err_dup "state" dup);
    1.82  
    1.83  fun the_state (id: Document.state_id) =
    1.84 -  (case Symtab.lookup (! global_states) id of
    1.85 +  (case Inttab.lookup (! global_states) id of
    1.86      NONE => err_undef "state" id
    1.87    | SOME state => state);
    1.88  
    1.89 @@ -139,23 +138,24 @@
    1.90  
    1.91  local
    1.92  
    1.93 -val global_commands = Unsynchronized.ref (Symtab.make [(Document.no_id, Toplevel.empty)]);
    1.94 +val global_commands = Unsynchronized.ref (Inttab.make [(Document.no_id, Toplevel.empty)]);
    1.95  
    1.96  in
    1.97  
    1.98  fun define_command (id: Document.command_id) text =
    1.99    let
   1.100 +    val id_string = Document.print_id id;
   1.101      val tr =
   1.102 -      Position.setmp_thread_data (Position.id_only id) (fn () =>
   1.103 -        Outer_Syntax.prepare_command (Position.id id) text) ();
   1.104 +      Position.setmp_thread_data (Position.id_only id_string) (fn () =>
   1.105 +        Outer_Syntax.prepare_command (Position.id id_string) text) ();
   1.106    in
   1.107      NAMED_CRITICAL "Isar" (fn () =>
   1.108 -      Unsynchronized.change global_commands (Symtab.update_new (id, Toplevel.put_id id tr))
   1.109 -        handle Symtab.DUP dup => err_dup "command" dup)
   1.110 +      Unsynchronized.change global_commands (Inttab.update_new (id, Toplevel.put_id id_string tr))
   1.111 +        handle Inttab.DUP dup => err_dup "command" dup)
   1.112    end;
   1.113  
   1.114  fun the_command (id: Document.command_id) =
   1.115 -  (case Symtab.lookup (! global_commands) id of
   1.116 +  (case Inttab.lookup (! global_commands) id of
   1.117      NONE => err_undef "command" id
   1.118    | SOME tr => tr);
   1.119  
   1.120 @@ -166,17 +166,17 @@
   1.121  
   1.122  local
   1.123  
   1.124 -val global_documents = Unsynchronized.ref (Symtab.make [(Document.no_id, Graph.empty: document)]);
   1.125 +val global_documents = Unsynchronized.ref (Inttab.make [(Document.no_id, Graph.empty: document)]);
   1.126  
   1.127  in
   1.128  
   1.129  fun define_document (id: Document.version_id) document =
   1.130    NAMED_CRITICAL "Isar" (fn () =>
   1.131 -    Unsynchronized.change global_documents (Symtab.update_new (id, document))
   1.132 -      handle Symtab.DUP dup => err_dup "document" dup);
   1.133 +    Unsynchronized.change global_documents (Inttab.update_new (id, document))
   1.134 +      handle Inttab.DUP dup => err_dup "document" dup);
   1.135  
   1.136  fun the_document (id: Document.version_id) =
   1.137 -  (case Symtab.lookup (! global_documents) id of
   1.138 +  (case Inttab.lookup (! global_documents) id of
   1.139      NONE => err_undef "document" id
   1.140    | SOME document => document);
   1.141  
   1.142 @@ -230,7 +230,7 @@
   1.143    let
   1.144      val state = the_state state_id;
   1.145      val state_id' = create_id ();
   1.146 -    val tr = Toplevel.put_id state_id' (the_command id);
   1.147 +    val tr = Toplevel.put_id (Document.print_id state_id') (the_command id);
   1.148      val state' =
   1.149        Lazy.lazy (fn () =>
   1.150          (case Lazy.force state of
   1.151 @@ -240,14 +240,15 @@
   1.152    in (state_id', (id, state_id') :: updates) end;
   1.153  
   1.154  fun updates_status updates =
   1.155 -  implode (map (fn (id, state_id) => Markup.markup (Markup.edit id state_id) "") updates)
   1.156 +  implode (map (fn (id, state_id) =>
   1.157 +    Markup.markup (Markup.edit (Document.print_id id) (Document.print_id state_id)) "") updates)
   1.158    |> Markup.markup Markup.assign
   1.159    |> Output.status;
   1.160  
   1.161  in
   1.162  
   1.163  fun edit_document (old_id: Document.version_id) (new_id: Document.version_id) edits =
   1.164 -  Position.setmp_thread_data (Position.id_only new_id) (fn () =>
   1.165 +  Position.setmp_thread_data (Position.id_only (Document.print_id new_id)) (fn () =>
   1.166      NAMED_CRITICAL "Isar" (fn () =>
   1.167        let
   1.168          val old_document = the_document old_id;
   1.169 @@ -281,16 +282,16 @@
   1.170  
   1.171  val _ =
   1.172    Isabelle_Process.add_command "Isar_Document.define_command"
   1.173 -    (fn [id, text] => define_command id text);
   1.174 +    (fn [id, text] => define_command (Document.parse_id id) text);
   1.175  
   1.176  val _ =
   1.177    Isabelle_Process.add_command "Isar_Document.edit_document"
   1.178      (fn [old_id, new_id, edits] =>
   1.179 -      edit_document old_id new_id
   1.180 +      edit_document (Document.parse_id old_id) (Document.parse_id new_id)
   1.181          (XML_Data.dest_list (XML_Data.dest_pair XML_Data.dest_string
   1.182              (XML_Data.dest_option (XML_Data.dest_list
   1.183 -                (XML_Data.dest_pair XML_Data.dest_string
   1.184 -                  (XML_Data.dest_option XML_Data.dest_string))))) (YXML.parse_body edits)));
   1.185 +                (XML_Data.dest_pair XML_Data.dest_int
   1.186 +                  (XML_Data.dest_option XML_Data.dest_int))))) (YXML.parse_body edits)));
   1.187  
   1.188  end;
   1.189