src/Pure/PIDE/document.ML
changeset 52530 99dd8b4ef3fe
parent 52527 dbac84eab3bc
child 52532 c81d76f7f63d
     1.1 --- a/src/Pure/PIDE/document.ML	Fri Jul 05 14:09:06 2013 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Fri Jul 05 15:38:03 2013 +0200
     1.3 @@ -7,31 +7,23 @@
     1.4  
     1.5  signature DOCUMENT =
     1.6  sig
     1.7 -  type id = int
     1.8 -  type version_id = id
     1.9 -  type command_id = id
    1.10 -  type exec_id = id
    1.11 -  val no_id: id
    1.12 -  val new_id: unit -> id
    1.13 -  val parse_id: string -> id
    1.14 -  val print_id: id -> string
    1.15    type node_header = string * Thy_Header.header * string list
    1.16    datatype node_edit =
    1.17      Clear |    (* FIXME unused !? *)
    1.18 -    Edits of (command_id option * command_id option) list |
    1.19 +    Edits of (Document_ID.command option * Document_ID.command option) list |
    1.20      Deps of node_header |
    1.21 -    Perspective of command_id list
    1.22 +    Perspective of Document_ID.command list
    1.23    type edit = string * node_edit
    1.24    type state
    1.25    val init_state: state
    1.26 -  val define_command: command_id -> string -> string -> state -> state
    1.27 -  val remove_versions: version_id list -> state -> state
    1.28 +  val define_command: Document_ID.command -> string -> string -> state -> state
    1.29 +  val remove_versions: Document_ID.version list -> state -> state
    1.30    val discontinue_execution: state -> unit
    1.31    val cancel_execution: state -> unit
    1.32    val start_execution: state -> unit
    1.33    val timing: bool Unsynchronized.ref
    1.34 -  val update: version_id -> version_id -> edit list -> state ->
    1.35 -    (command_id * exec_id list) list * state
    1.36 +  val update: Document_ID.version -> Document_ID.version -> edit list -> state ->
    1.37 +    (Document_ID.command * Document_ID.exec list) list * state
    1.38    val state: unit -> state
    1.39    val change_state: (state -> state) -> unit
    1.40  end;
    1.41 @@ -39,27 +31,10 @@
    1.42  structure Document: DOCUMENT =
    1.43  struct
    1.44  
    1.45 -(* unique identifiers *)
    1.46 -
    1.47 -type id = int;
    1.48 -type version_id = id;
    1.49 -type command_id = id;
    1.50 -type exec_id = id;
    1.51 -
    1.52 -val no_id = 0;
    1.53 -val new_id = Synchronized.counter ();
    1.54 -
    1.55 -val parse_id = Markup.parse_int;
    1.56 -val print_id = Markup.print_int;
    1.57 -
    1.58 -fun err_dup kind id = error ("Duplicate " ^ kind ^ ": " ^ print_id id);
    1.59 -fun err_undef kind id = error ("Undefined " ^ kind ^ ": " ^ print_id id);
    1.60 -
    1.61 -
    1.62  (* command execution *)
    1.63  
    1.64 -type exec = exec_id * (Command.eval * Command.print list);  (*eval/print process*)
    1.65 -val no_exec: exec = (no_id, (Command.no_eval, []));
    1.66 +type exec = Document_ID.exec * (Command.eval * Command.print list);  (*eval/print process*)
    1.67 +val no_exec: exec = (Document_ID.none, (Command.no_eval, []));
    1.68  
    1.69  fun exec_ids_of ((exec_id, (_, prints)): exec) = exec_id :: map #exec_id prints;
    1.70  
    1.71 @@ -74,9 +49,12 @@
    1.72  
    1.73  (** document structure **)
    1.74  
    1.75 +fun err_dup kind id = error ("Duplicate " ^ kind ^ ": " ^ Document_ID.print id);
    1.76 +fun err_undef kind id = error ("Undefined " ^ kind ^ ": " ^ Document_ID.print id);
    1.77 +
    1.78  type node_header = string * Thy_Header.header * string list;
    1.79 -type perspective = Inttab.set * command_id option;
    1.80 -structure Entries = Linear_Set(type key = command_id val ord = int_ord);
    1.81 +type perspective = Inttab.set * Document_ID.command option;
    1.82 +structure Entries = Linear_Set(type key = Document_ID.command val ord = int_ord);
    1.83  
    1.84  abstype node = Node of
    1.85   {header: node_header,  (*master directory, theory header, errors*)
    1.86 @@ -156,9 +134,9 @@
    1.87  
    1.88  datatype node_edit =
    1.89    Clear |
    1.90 -  Edits of (command_id option * command_id option) list |
    1.91 +  Edits of (Document_ID.command option * Document_ID.command option) list |
    1.92    Deps of node_header |
    1.93 -  Perspective of command_id list;
    1.94 +  Perspective of Document_ID.command list;
    1.95  
    1.96  type edit = string * node_edit;
    1.97  
    1.98 @@ -175,7 +153,7 @@
    1.99    | SOME (exec, _) => exec);
   1.100  
   1.101  fun the_default_entry node (SOME id) = (id, the_default no_exec (the_entry node id))
   1.102 -  | the_default_entry _ NONE = (no_id, no_exec);
   1.103 +  | the_default_entry _ NONE = (Document_ID.none, no_exec);
   1.104  
   1.105  fun update_entry id exec =
   1.106    map_entries (Entries.update (id, exec));
   1.107 @@ -237,7 +215,8 @@
   1.108  abstype state = State of
   1.109   {versions: version Inttab.table,  (*version_id -> document content*)
   1.110    commands: (string * Token.T list lazy) Inttab.table,  (*command_id -> named span*)
   1.111 -  execution: version_id * Future.group * bool Unsynchronized.ref}  (*current execution process*)
   1.112 +  execution:
   1.113 +    Document_ID.version * Future.group * bool Unsynchronized.ref}  (*current execution process*)
   1.114  with
   1.115  
   1.116  fun make_state (versions, commands, execution) =
   1.117 @@ -247,15 +226,15 @@
   1.118    make_state (f (versions, commands, execution));
   1.119  
   1.120  val init_state =
   1.121 -  make_state (Inttab.make [(no_id, empty_version)], Inttab.empty,
   1.122 -    (no_id, Future.new_group NONE, Unsynchronized.ref false));
   1.123 +  make_state (Inttab.make [(Document_ID.none, empty_version)], Inttab.empty,
   1.124 +    (Document_ID.none, Future.new_group NONE, Unsynchronized.ref false));
   1.125  
   1.126  fun execution_of (State {execution, ...}) = execution;
   1.127  
   1.128  
   1.129  (* document versions *)
   1.130  
   1.131 -fun define_version (id: version_id) version =
   1.132 +fun define_version (id: Document_ID.version) version =
   1.133    map_state (fn (versions, commands, _) =>
   1.134      let
   1.135        val versions' = Inttab.update_new (id, version) versions
   1.136 @@ -263,21 +242,21 @@
   1.137        val execution' = (id, Future.new_group NONE, Unsynchronized.ref true);
   1.138      in (versions', commands, execution') end);
   1.139  
   1.140 -fun the_version (State {versions, ...}) (id: version_id) =
   1.141 +fun the_version (State {versions, ...}) (id: Document_ID.version) =
   1.142    (case Inttab.lookup versions id of
   1.143      NONE => err_undef "document version" id
   1.144    | SOME version => version);
   1.145  
   1.146 -fun delete_version (id: version_id) versions = Inttab.delete id versions
   1.147 +fun delete_version (id: Document_ID.version) versions = Inttab.delete id versions
   1.148    handle Inttab.UNDEF _ => err_undef "document version" id;
   1.149  
   1.150  
   1.151  (* commands *)
   1.152  
   1.153 -fun define_command (id: command_id) name text =
   1.154 +fun define_command (id: Document_ID.command) name text =
   1.155    map_state (fn (versions, commands, execution) =>
   1.156      let
   1.157 -      val id_string = print_id id;
   1.158 +      val id_string = Document_ID.print id;
   1.159        val span = Lazy.lazy (fn () =>
   1.160          Position.setmp_thread_data (Position.id_only id_string)
   1.161            (fn () => Thy_Syntax.parse_tokens (Keyword.get_lexicons ()) (Position.id id_string) text)
   1.162 @@ -290,7 +269,7 @@
   1.163            handle Inttab.DUP dup => err_dup "command" dup;
   1.164      in (versions, commands', execution) end);
   1.165  
   1.166 -fun the_command (State {commands, ...}) (id: command_id) =
   1.167 +fun the_command (State {commands, ...}) (id: Document_ID.command) =
   1.168    (case Inttab.lookup commands id of
   1.169      NONE => err_undef "command" id
   1.170    | SOME command => command);
   1.171 @@ -300,7 +279,7 @@
   1.172  fun remove_versions ids state = state |> map_state (fn (versions, _, execution) =>
   1.173    let
   1.174      val _ = member (op =) ids (#1 execution) andalso
   1.175 -      error ("Attempt to remove execution version " ^ print_id (#1 execution));
   1.176 +      error ("Attempt to remove execution version " ^ Document_ID.print (#1 execution));
   1.177  
   1.178      val versions' = fold delete_version ids versions;
   1.179      val commands' =
   1.180 @@ -451,19 +430,19 @@
   1.181            (Toplevel.modify_init (fn () => the_default illegal_init init span), NONE)
   1.182          else (I, init);
   1.183  
   1.184 -      val exec_id' = new_id ();
   1.185 +      val exec_id' = Document_ID.make ();
   1.186        val eval' =
   1.187          Command.memo (fn () =>
   1.188            let
   1.189              val eval_state = exec_result (snd command_exec);
   1.190              val tr =
   1.191 -              Position.setmp_thread_data (Position.id_only (print_id exec_id'))
   1.192 +              Position.setmp_thread_data (Position.id_only (Document_ID.print exec_id'))
   1.193                  (fn () =>
   1.194                    Command.read span
   1.195                    |> modify_init
   1.196                    |> Toplevel.put_id exec_id') ();
   1.197            in Command.eval span tr eval_state end);
   1.198 -      val prints' = if command_visible then Command.print new_id command_name eval' else [];
   1.199 +      val prints' = if command_visible then Command.print command_name eval' else [];
   1.200        val command_exec' = (command_id', (exec_id', (eval', prints')));
   1.201      in SOME (command_exec' :: execs, command_exec', init') end;
   1.202  
   1.203 @@ -472,7 +451,7 @@
   1.204      SOME (exec_id, (eval, prints)) =>
   1.205        let
   1.206          val (command_name, _) = the_command state command_id;
   1.207 -        val new_prints = Command.print new_id command_name eval;
   1.208 +        val new_prints = Command.print command_name eval;
   1.209          val prints' =
   1.210            new_prints |> map (fn new_print =>
   1.211              (case find_first (fn {name, ...} => name = #name new_print) prints of
   1.212 @@ -486,7 +465,7 @@
   1.213  
   1.214  in
   1.215  
   1.216 -fun update (old_id: version_id) (new_id: version_id) edits state =
   1.217 +fun update (old_id: Document_ID.version) (new_id: Document_ID.version) edits state =
   1.218    let
   1.219      val old_version = the_version state old_id;
   1.220      val new_version = timeit "Document.edit_nodes" (fn () => fold edit_nodes edits old_version);
   1.221 @@ -547,7 +526,8 @@
   1.222                            then SOME res
   1.223                            else SOME (id0 :: res)) node0 [];
   1.224  
   1.225 -                    val last_exec = if command_id' = no_id then NONE else SOME command_id';
   1.226 +                    val last_exec =
   1.227 +                      if command_id' = Document_ID.none then NONE else SOME command_id';
   1.228                      val result =
   1.229                        if is_some (after_entry node last_exec) then NONE
   1.230                        else SOME eval';