src/Pure/PIDE/document.ML
changeset 52536 3a35ce87a55c
parent 52534 341ae9cd4743
child 52566 52a0eacf04d1
     1.1 --- a/src/Pure/PIDE/document.ML	Fri Jul 05 22:09:16 2013 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Fri Jul 05 22:58:24 2013 +0200
     1.3 @@ -2,7 +2,7 @@
     1.4      Author:     Makarius
     1.5  
     1.6  Document as collection of named nodes, each consisting of an editable
     1.7 -list of commands, with asynchronous read/eval/print processes.
     1.8 +list of commands, associated with asynchronous execution process.
     1.9  *)
    1.10  
    1.11  signature DOCUMENT =
    1.12 @@ -201,11 +201,20 @@
    1.13  
    1.14  (** main state -- document structure and execution process **)
    1.15  
    1.16 +type execution =
    1.17 + {version_id: Document_ID.version,
    1.18 +  group: Future.group,
    1.19 +  running: bool Unsynchronized.ref};
    1.20 +
    1.21 +val no_execution =
    1.22 + {version_id = Document_ID.none,
    1.23 +  group = Future.new_group NONE,
    1.24 +  running = Unsynchronized.ref false};
    1.25 +
    1.26  abstype state = State of
    1.27 - {versions: version Inttab.table,  (*version_id -> document content*)
    1.28 -  commands: (string * Token.T list lazy) Inttab.table,  (*command_id -> named span*)
    1.29 -  execution:
    1.30 -    Document_ID.version * Future.group * bool Unsynchronized.ref}  (*current execution process*)
    1.31 + {versions: version Inttab.table,  (*version id -> document content*)
    1.32 +  commands: (string * Token.T list lazy) Inttab.table,  (*command id -> named span*)
    1.33 +  execution: execution}  (*current execution process*)
    1.34  with
    1.35  
    1.36  fun make_state (versions, commands, execution) =
    1.37 @@ -215,81 +224,85 @@
    1.38    make_state (f (versions, commands, execution));
    1.39  
    1.40  val init_state =
    1.41 -  make_state (Inttab.make [(Document_ID.none, empty_version)], Inttab.empty,
    1.42 -    (Document_ID.none, Future.new_group NONE, Unsynchronized.ref false));
    1.43 +  make_state (Inttab.make [(Document_ID.none, empty_version)], Inttab.empty, no_execution);
    1.44  
    1.45  fun execution_of (State {execution, ...}) = execution;
    1.46  
    1.47  
    1.48  (* document versions *)
    1.49  
    1.50 -fun define_version (id: Document_ID.version) version =
    1.51 +fun define_version version_id version =
    1.52    map_state (fn (versions, commands, _) =>
    1.53      let
    1.54 -      val versions' = Inttab.update_new (id, version) versions
    1.55 +      val versions' = Inttab.update_new (version_id, version) versions
    1.56          handle Inttab.DUP dup => err_dup "document version" dup;
    1.57 -      val execution' = (id, Future.new_group NONE, Unsynchronized.ref true);
    1.58 +      val execution' =
    1.59 +       {version_id = version_id,
    1.60 +        group = Future.new_group NONE,
    1.61 +        running = Unsynchronized.ref true};
    1.62      in (versions', commands, execution') end);
    1.63  
    1.64 -fun the_version (State {versions, ...}) (id: Document_ID.version) =
    1.65 -  (case Inttab.lookup versions id of
    1.66 -    NONE => err_undef "document version" id
    1.67 +fun the_version (State {versions, ...}) version_id =
    1.68 +  (case Inttab.lookup versions version_id of
    1.69 +    NONE => err_undef "document version" version_id
    1.70    | SOME version => version);
    1.71  
    1.72 -fun delete_version (id: Document_ID.version) versions = Inttab.delete id versions
    1.73 -  handle Inttab.UNDEF _ => err_undef "document version" id;
    1.74 +fun delete_version version_id versions =
    1.75 +  Inttab.delete version_id versions
    1.76 +    handle Inttab.UNDEF _ => err_undef "document version" version_id;
    1.77  
    1.78  
    1.79  (* commands *)
    1.80  
    1.81 -fun define_command (id: Document_ID.command) name text =
    1.82 +fun define_command command_id name text =
    1.83    map_state (fn (versions, commands, execution) =>
    1.84      let
    1.85 -      val id_string = Document_ID.print id;
    1.86 -      val span = Lazy.lazy (fn () =>
    1.87 -        Position.setmp_thread_data (Position.id_only id_string)
    1.88 -          (fn () => Thy_Syntax.parse_tokens (Keyword.get_lexicons ()) (Position.id id_string) text)
    1.89 -            ());
    1.90 +      val id = Document_ID.print command_id;
    1.91 +      val span =
    1.92 +        Lazy.lazy (fn () =>
    1.93 +          Position.setmp_thread_data (Position.id_only id)
    1.94 +            (fn () => Thy_Syntax.parse_tokens (Keyword.get_lexicons ()) (Position.id id) text) ());
    1.95        val _ =
    1.96 -        Position.setmp_thread_data (Position.id_only id_string)
    1.97 +        Position.setmp_thread_data (Position.id_only id)
    1.98            (fn () => Output.status (Markup.markup_only Markup.accepted)) ();
    1.99        val commands' =
   1.100 -        Inttab.update_new (id, (name, span)) commands
   1.101 +        Inttab.update_new (command_id, (name, span)) commands
   1.102            handle Inttab.DUP dup => err_dup "command" dup;
   1.103      in (versions, commands', execution) end);
   1.104  
   1.105 -fun the_command (State {commands, ...}) (id: Document_ID.command) =
   1.106 -  (case Inttab.lookup commands id of
   1.107 -    NONE => err_undef "command" id
   1.108 +fun the_command (State {commands, ...}) command_id =
   1.109 +  (case Inttab.lookup commands command_id of
   1.110 +    NONE => err_undef "command" command_id
   1.111    | SOME command => command);
   1.112  
   1.113  end;
   1.114  
   1.115 -fun remove_versions ids state = state |> map_state (fn (versions, _, execution) =>
   1.116 +fun remove_versions version_ids state = state |> map_state (fn (versions, _, execution) =>
   1.117    let
   1.118 -    val _ = member (op =) ids (#1 execution) andalso
   1.119 -      error ("Attempt to remove execution version " ^ Document_ID.print (#1 execution));
   1.120 +    val _ =
   1.121 +      member (op =) version_ids (#version_id execution) andalso
   1.122 +        error ("Attempt to remove execution version " ^ Document_ID.print (#version_id execution));
   1.123  
   1.124 -    val versions' = fold delete_version ids versions;
   1.125 +    val versions' = fold delete_version version_ids versions;
   1.126      val commands' =
   1.127        (versions', Inttab.empty) |->
   1.128          Inttab.fold (fn (_, version) => nodes_of version |>
   1.129            String_Graph.fold (fn (_, (node, _)) => node |>
   1.130 -            iterate_entries (fn ((_, id), _) =>
   1.131 -              SOME o Inttab.insert (K true) (id, the_command state id))));
   1.132 +            iterate_entries (fn ((_, command_id), _) =>
   1.133 +              SOME o Inttab.insert (K true) (command_id, the_command state command_id))));
   1.134    in (versions', commands', execution) end);
   1.135  
   1.136  
   1.137  
   1.138  (** document execution **)
   1.139  
   1.140 -val discontinue_execution = execution_of #> (fn (_, _, running) => running := false);
   1.141 -val cancel_execution = execution_of #> (fn (_, group, _) => Future.cancel_group group);
   1.142 -val terminate_execution = execution_of #> (fn (_, group, _) => Future.terminate group);
   1.143 +val discontinue_execution = execution_of #> (fn {running, ...} => running := false);
   1.144 +val cancel_execution = execution_of #> (fn {group, ...} => Future.cancel_group group);
   1.145 +val terminate_execution = execution_of #> (fn {group, ...} => Future.terminate group);
   1.146  
   1.147  fun start_execution state =
   1.148    let
   1.149 -    val (version_id, group, running) = execution_of state;
   1.150 +    val {version_id, group, running} = execution_of state;
   1.151      val _ =
   1.152        (singleton o Future.forks)
   1.153          {name = "Document.execution", group = SOME group, deps = [], pri = ~2, interrupts = true}
   1.154 @@ -306,7 +319,7 @@
   1.155                    (fn () =>
   1.156                      iterate_entries (fn (_, opt_exec) => fn () =>
   1.157                        (case opt_exec of
   1.158 -                        SOME exec => if ! running then SOME (Command.exec_run exec) else NONE
   1.159 +                        SOME exec => if ! running then SOME (Command.execute exec) else NONE
   1.160                        | NONE => NONE)) node ()))));
   1.161    in () end;
   1.162  
   1.163 @@ -347,9 +360,9 @@
   1.164            SOME thy => thy
   1.165          | NONE =>
   1.166              Toplevel.end_theory (Position.file_only import)
   1.167 -              (Command.eval_result_state
   1.168 -                (the_default Command.no_eval
   1.169 -                  (get_result (snd (the (AList.lookup (op =) deps import))))))));
   1.170 +              (case get_result (snd (the (AList.lookup (op =) deps import))) of
   1.171 +                NONE => Toplevel.toplevel
   1.172 +              | SOME eval => Command.eval_result_state eval)));
   1.173      val _ = Position.reports (map #2 imports ~~ map Theory.get_markup parents);
   1.174    in Thy_Load.begin_theory master_dir header parents end;
   1.175  
   1.176 @@ -423,9 +436,9 @@
   1.177  
   1.178  in
   1.179  
   1.180 -fun update (old_id: Document_ID.version) (new_id: Document_ID.version) edits state =
   1.181 +fun update old_version_id new_version_id edits state =
   1.182    let
   1.183 -    val old_version = the_version state old_id;
   1.184 +    val old_version = the_version state old_version_id;
   1.185      val new_version = timeit "Document.edit_nodes" (fn () => fold edit_nodes edits old_version);
   1.186  
   1.187      val nodes = nodes_of new_version;
   1.188 @@ -510,7 +523,7 @@
   1.189      val updated_nodes = map_filter #3 updated;
   1.190  
   1.191      val state' = state
   1.192 -      |> define_version new_id (fold put_node updated_nodes new_version);
   1.193 +      |> define_version new_version_id (fold put_node updated_nodes new_version);
   1.194    in (command_execs, state') end;
   1.195  
   1.196  end;