tuned signature;
authorwenzelm
Fri Jul 05 22:58:24 2013 +0200 (2013-07-05)
changeset 525363a35ce87a55c
parent 52535 b7badd371e4d
child 52537 4b5941730bd8
tuned signature;
tuned comments;
src/Pure/Isar/toplevel.ML
src/Pure/PIDE/command.ML
src/Pure/PIDE/command.scala
src/Pure/PIDE/document.ML
src/Pure/ROOT.ML
     1.1 --- a/src/Pure/Isar/toplevel.ML	Fri Jul 05 22:09:16 2013 +0200
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Fri Jul 05 22:58:24 2013 +0200
     1.3 @@ -81,7 +81,7 @@
     1.4    val actual_proof: (Proof_Node.T -> Proof_Node.T) -> transition -> transition
     1.5    val skip_proof: (int -> int) -> transition -> transition
     1.6    val skip_proof_to_theory: (int -> bool) -> transition -> transition
     1.7 -  val put_id: int -> transition -> transition
     1.8 +  val exec_id: Document_ID.exec -> transition -> transition
     1.9    val unknown_theory: transition -> transition
    1.10    val unknown_proof: transition -> transition
    1.11    val unknown_context: transition -> transition
    1.12 @@ -585,8 +585,8 @@
    1.13  
    1.14  (* runtime position *)
    1.15  
    1.16 -fun put_id id (tr as Transition {pos, ...}) =
    1.17 -  position (Position.put_id (Markup.print_int id) pos) tr;
    1.18 +fun exec_id id (tr as Transition {pos, ...}) =
    1.19 +  position (Position.put_id (Document_ID.print id) pos) tr;
    1.20  
    1.21  fun setmp_thread_position (Transition {pos, ...}) f x =
    1.22    Position.setmp_thread_data pos f x;
     2.1 --- a/src/Pure/PIDE/command.ML	Fri Jul 05 22:09:16 2013 +0200
     2.2 +++ b/src/Pure/PIDE/command.ML	Fri Jul 05 22:58:24 2013 +0200
     2.3 @@ -8,19 +8,18 @@
     2.4  sig
     2.5    type eval_process
     2.6    type eval = {exec_id: Document_ID.exec, eval_process: eval_process}
     2.7 +  val eval_result_state: eval -> Toplevel.state
     2.8    type print_process
     2.9    type print = {name: string, pri: int, exec_id: Document_ID.exec, print_process: print_process}
    2.10    type exec = eval * print list
    2.11 +  val no_exec: exec
    2.12 +  val exec_ids: exec -> Document_ID.exec list
    2.13    val read: (unit -> theory) -> Token.T list -> Toplevel.transition
    2.14 -  val no_eval: eval
    2.15 -  val eval_result_state: eval -> Toplevel.state
    2.16    val eval: (unit -> theory) -> Token.T list -> eval -> eval
    2.17    val print: string -> eval -> print list
    2.18    type print_fn = Toplevel.transition -> Toplevel.state -> unit
    2.19    val print_function: {name: string, pri: int} -> (string -> print_fn option) -> unit
    2.20 -  val no_exec: exec
    2.21 -  val exec_ids: exec -> Document_ID.exec list
    2.22 -  val exec_run: exec -> unit
    2.23 +  val execute: exec -> unit
    2.24    val stable_eval: eval -> bool
    2.25    val stable_print: print -> bool
    2.26  end;
    2.27 @@ -70,16 +69,29 @@
    2.28  
    2.29  
    2.30  
    2.31 -(** main phases **)
    2.32 +(** main phases of execution **)
    2.33 +
    2.34 +(* basic type definitions *)
    2.35  
    2.36  type eval_state =
    2.37    {failed: bool, malformed: bool, command: Toplevel.transition, state: Toplevel.state};
    2.38 +val init_eval_state =
    2.39 +  {failed = false, malformed = false, command = Toplevel.empty, state = Toplevel.toplevel};
    2.40 +
    2.41  type eval_process = eval_state memo;
    2.42  type eval = {exec_id: Document_ID.exec, eval_process: eval_process};
    2.43  
    2.44 +fun eval_result ({eval_process, ...}: eval) = memo_result eval_process;
    2.45 +val eval_result_state = #state o eval_result;
    2.46 +
    2.47  type print_process = unit memo;
    2.48  type print = {name: string, pri: int, exec_id: Document_ID.exec, print_process: print_process};
    2.49  
    2.50 +type exec = eval * print list;
    2.51 +val no_exec: exec = ({exec_id = Document_ID.none, eval_process = memo_value init_eval_state}, []);
    2.52 +
    2.53 +fun exec_ids (({exec_id, ...}, prints): exec) = exec_id :: map #exec_id prints;
    2.54 +
    2.55  
    2.56  (* read *)
    2.57  
    2.58 @@ -113,14 +125,6 @@
    2.59  
    2.60  (* eval *)
    2.61  
    2.62 -val no_eval_state: eval_state =
    2.63 -  {failed = false, malformed = false, command = Toplevel.empty, state = Toplevel.toplevel};
    2.64 -
    2.65 -val no_eval: eval = {exec_id = Document_ID.none, eval_process = memo_value no_eval_state};
    2.66 -
    2.67 -fun eval_result ({eval_process, ...}: eval) = memo_result eval_process;
    2.68 -val eval_result_state = #state o eval_result;
    2.69 -
    2.70  local
    2.71  
    2.72  fun run int tr st =
    2.73 @@ -179,7 +183,7 @@
    2.74        let
    2.75          val tr =
    2.76            Position.setmp_thread_data (Position.id_only (Document_ID.print exec_id))
    2.77 -            (fn () => read init span |> Toplevel.put_id exec_id) ();
    2.78 +            (fn () => read init span |> Toplevel.exec_id exec_id) ();
    2.79        in eval_state span tr (eval_result eval0) end;
    2.80    in {exec_id = exec_id, eval_process = memo process} end;
    2.81  
    2.82 @@ -214,7 +218,7 @@
    2.83            fun process () =
    2.84              let
    2.85                val {failed, command, state = st', ...} = eval_result eval;
    2.86 -              val tr = Toplevel.put_id exec_id command;
    2.87 +              val tr = Toplevel.exec_id exec_id command;
    2.88              in if failed then () else print_error tr (fn () => print_fn tr st') () end;
    2.89          in SOME {name = name, pri = pri, exec_id = exec_id, print_process = memo process} end
    2.90      | Exn.Exn exn =>
    2.91 @@ -223,7 +227,7 @@
    2.92            fun process () =
    2.93              let
    2.94                val {command, ...} = eval_result eval;
    2.95 -              val tr = Toplevel.put_id exec_id command;
    2.96 +              val tr = Toplevel.exec_id exec_id command;
    2.97              in output_error tr exn end;
    2.98          in SOME {name = name, pri = pri, exec_id = exec_id, print_process = memo process} end));
    2.99  
   2.100 @@ -246,24 +250,13 @@
   2.101      in if do_print then Toplevel.print_state false st' else () end));
   2.102  
   2.103  
   2.104 -
   2.105 -(** managed evaluation **)
   2.106 -
   2.107 -(* execution *)
   2.108 +(* overall execution process *)
   2.109  
   2.110 -type exec = eval * print list;
   2.111 -val no_exec: exec = (no_eval, []);
   2.112 -
   2.113 -fun exec_ids (({exec_id, ...}, prints): exec) = exec_id :: map #exec_id prints;
   2.114 -
   2.115 -fun exec_run (({eval_process, ...}, prints): exec) =
   2.116 +fun execute (({eval_process, ...}, prints): exec) =
   2.117   (memo_eval eval_process;
   2.118    prints |> List.app (fn {name, pri, print_process, ...} =>
   2.119      memo_fork {name = name, group = NONE, deps = [], pri = pri, interrupts = true} print_process));
   2.120  
   2.121 -
   2.122 -(* stable situations after cancellation *)
   2.123 -
   2.124  fun stable_goals exec_id =
   2.125    not (Par_Exn.is_interrupted (Future.join_results (Goal.peek_futures exec_id)));
   2.126  
     3.1 --- a/src/Pure/PIDE/command.scala	Fri Jul 05 22:09:16 2013 +0200
     3.2 +++ b/src/Pure/PIDE/command.scala	Fri Jul 05 22:58:24 2013 +0200
     3.3 @@ -2,12 +2,11 @@
     3.4      Author:     Fabian Immler, TU Munich
     3.5      Author:     Makarius
     3.6  
     3.7 -Prover commands with semantic state.
     3.8 +Prover commands with accumulated results from execution.
     3.9  */
    3.10  
    3.11  package isabelle
    3.12  
    3.13 -import java.lang.System
    3.14  
    3.15  import scala.collection.mutable
    3.16  import scala.collection.immutable.SortedMap
    3.17 @@ -84,7 +83,9 @@
    3.18                  state.add_status(markup)
    3.19                    .add_markup(Text.Info(command.proper_range, elem))  // FIXME cumulation order!?
    3.20  
    3.21 -              case _ => System.err.println("Ignored status message: " + msg); state
    3.22 +              case _ =>
    3.23 +                java.lang.System.err.println("Ignored status message: " + msg)
    3.24 +                state
    3.25              })
    3.26  
    3.27          case XML.Elem(Markup(Markup.REPORT, _), msgs) =>
    3.28 @@ -104,7 +105,7 @@
    3.29                  val info: Text.Markup = Text.Info(range, XML.Elem(Markup(name, props), args))
    3.30                  state.add_markup(info)
    3.31                case _ =>
    3.32 -                // FIXME System.err.println("Ignored report message: " + msg)
    3.33 +                // FIXME java.lang.System.err.println("Ignored report message: " + msg)
    3.34                  state
    3.35              })
    3.36          case XML.Elem(Markup(name, atts), body) =>
    3.37 @@ -122,7 +123,9 @@
    3.38                  else st0
    3.39  
    3.40                st1
    3.41 -            case _ => System.err.println("Ignored message without serial number: " + message); this
    3.42 +            case _ =>
    3.43 +              java.lang.System.err.println("Ignored message without serial number: " + message)
    3.44 +              this
    3.45            }
    3.46        }
    3.47  
     4.1 --- a/src/Pure/PIDE/document.ML	Fri Jul 05 22:09:16 2013 +0200
     4.2 +++ b/src/Pure/PIDE/document.ML	Fri Jul 05 22:58:24 2013 +0200
     4.3 @@ -2,7 +2,7 @@
     4.4      Author:     Makarius
     4.5  
     4.6  Document as collection of named nodes, each consisting of an editable
     4.7 -list of commands, with asynchronous read/eval/print processes.
     4.8 +list of commands, associated with asynchronous execution process.
     4.9  *)
    4.10  
    4.11  signature DOCUMENT =
    4.12 @@ -201,11 +201,20 @@
    4.13  
    4.14  (** main state -- document structure and execution process **)
    4.15  
    4.16 +type execution =
    4.17 + {version_id: Document_ID.version,
    4.18 +  group: Future.group,
    4.19 +  running: bool Unsynchronized.ref};
    4.20 +
    4.21 +val no_execution =
    4.22 + {version_id = Document_ID.none,
    4.23 +  group = Future.new_group NONE,
    4.24 +  running = Unsynchronized.ref false};
    4.25 +
    4.26  abstype state = State of
    4.27 - {versions: version Inttab.table,  (*version_id -> document content*)
    4.28 -  commands: (string * Token.T list lazy) Inttab.table,  (*command_id -> named span*)
    4.29 -  execution:
    4.30 -    Document_ID.version * Future.group * bool Unsynchronized.ref}  (*current execution process*)
    4.31 + {versions: version Inttab.table,  (*version id -> document content*)
    4.32 +  commands: (string * Token.T list lazy) Inttab.table,  (*command id -> named span*)
    4.33 +  execution: execution}  (*current execution process*)
    4.34  with
    4.35  
    4.36  fun make_state (versions, commands, execution) =
    4.37 @@ -215,81 +224,85 @@
    4.38    make_state (f (versions, commands, execution));
    4.39  
    4.40  val init_state =
    4.41 -  make_state (Inttab.make [(Document_ID.none, empty_version)], Inttab.empty,
    4.42 -    (Document_ID.none, Future.new_group NONE, Unsynchronized.ref false));
    4.43 +  make_state (Inttab.make [(Document_ID.none, empty_version)], Inttab.empty, no_execution);
    4.44  
    4.45  fun execution_of (State {execution, ...}) = execution;
    4.46  
    4.47  
    4.48  (* document versions *)
    4.49  
    4.50 -fun define_version (id: Document_ID.version) version =
    4.51 +fun define_version version_id version =
    4.52    map_state (fn (versions, commands, _) =>
    4.53      let
    4.54 -      val versions' = Inttab.update_new (id, version) versions
    4.55 +      val versions' = Inttab.update_new (version_id, version) versions
    4.56          handle Inttab.DUP dup => err_dup "document version" dup;
    4.57 -      val execution' = (id, Future.new_group NONE, Unsynchronized.ref true);
    4.58 +      val execution' =
    4.59 +       {version_id = version_id,
    4.60 +        group = Future.new_group NONE,
    4.61 +        running = Unsynchronized.ref true};
    4.62      in (versions', commands, execution') end);
    4.63  
    4.64 -fun the_version (State {versions, ...}) (id: Document_ID.version) =
    4.65 -  (case Inttab.lookup versions id of
    4.66 -    NONE => err_undef "document version" id
    4.67 +fun the_version (State {versions, ...}) version_id =
    4.68 +  (case Inttab.lookup versions version_id of
    4.69 +    NONE => err_undef "document version" version_id
    4.70    | SOME version => version);
    4.71  
    4.72 -fun delete_version (id: Document_ID.version) versions = Inttab.delete id versions
    4.73 -  handle Inttab.UNDEF _ => err_undef "document version" id;
    4.74 +fun delete_version version_id versions =
    4.75 +  Inttab.delete version_id versions
    4.76 +    handle Inttab.UNDEF _ => err_undef "document version" version_id;
    4.77  
    4.78  
    4.79  (* commands *)
    4.80  
    4.81 -fun define_command (id: Document_ID.command) name text =
    4.82 +fun define_command command_id name text =
    4.83    map_state (fn (versions, commands, execution) =>
    4.84      let
    4.85 -      val id_string = Document_ID.print id;
    4.86 -      val span = Lazy.lazy (fn () =>
    4.87 -        Position.setmp_thread_data (Position.id_only id_string)
    4.88 -          (fn () => Thy_Syntax.parse_tokens (Keyword.get_lexicons ()) (Position.id id_string) text)
    4.89 -            ());
    4.90 +      val id = Document_ID.print command_id;
    4.91 +      val span =
    4.92 +        Lazy.lazy (fn () =>
    4.93 +          Position.setmp_thread_data (Position.id_only id)
    4.94 +            (fn () => Thy_Syntax.parse_tokens (Keyword.get_lexicons ()) (Position.id id) text) ());
    4.95        val _ =
    4.96 -        Position.setmp_thread_data (Position.id_only id_string)
    4.97 +        Position.setmp_thread_data (Position.id_only id)
    4.98            (fn () => Output.status (Markup.markup_only Markup.accepted)) ();
    4.99        val commands' =
   4.100 -        Inttab.update_new (id, (name, span)) commands
   4.101 +        Inttab.update_new (command_id, (name, span)) commands
   4.102            handle Inttab.DUP dup => err_dup "command" dup;
   4.103      in (versions, commands', execution) end);
   4.104  
   4.105 -fun the_command (State {commands, ...}) (id: Document_ID.command) =
   4.106 -  (case Inttab.lookup commands id of
   4.107 -    NONE => err_undef "command" id
   4.108 +fun the_command (State {commands, ...}) command_id =
   4.109 +  (case Inttab.lookup commands command_id of
   4.110 +    NONE => err_undef "command" command_id
   4.111    | SOME command => command);
   4.112  
   4.113  end;
   4.114  
   4.115 -fun remove_versions ids state = state |> map_state (fn (versions, _, execution) =>
   4.116 +fun remove_versions version_ids state = state |> map_state (fn (versions, _, execution) =>
   4.117    let
   4.118 -    val _ = member (op =) ids (#1 execution) andalso
   4.119 -      error ("Attempt to remove execution version " ^ Document_ID.print (#1 execution));
   4.120 +    val _ =
   4.121 +      member (op =) version_ids (#version_id execution) andalso
   4.122 +        error ("Attempt to remove execution version " ^ Document_ID.print (#version_id execution));
   4.123  
   4.124 -    val versions' = fold delete_version ids versions;
   4.125 +    val versions' = fold delete_version version_ids versions;
   4.126      val commands' =
   4.127        (versions', Inttab.empty) |->
   4.128          Inttab.fold (fn (_, version) => nodes_of version |>
   4.129            String_Graph.fold (fn (_, (node, _)) => node |>
   4.130 -            iterate_entries (fn ((_, id), _) =>
   4.131 -              SOME o Inttab.insert (K true) (id, the_command state id))));
   4.132 +            iterate_entries (fn ((_, command_id), _) =>
   4.133 +              SOME o Inttab.insert (K true) (command_id, the_command state command_id))));
   4.134    in (versions', commands', execution) end);
   4.135  
   4.136  
   4.137  
   4.138  (** document execution **)
   4.139  
   4.140 -val discontinue_execution = execution_of #> (fn (_, _, running) => running := false);
   4.141 -val cancel_execution = execution_of #> (fn (_, group, _) => Future.cancel_group group);
   4.142 -val terminate_execution = execution_of #> (fn (_, group, _) => Future.terminate group);
   4.143 +val discontinue_execution = execution_of #> (fn {running, ...} => running := false);
   4.144 +val cancel_execution = execution_of #> (fn {group, ...} => Future.cancel_group group);
   4.145 +val terminate_execution = execution_of #> (fn {group, ...} => Future.terminate group);
   4.146  
   4.147  fun start_execution state =
   4.148    let
   4.149 -    val (version_id, group, running) = execution_of state;
   4.150 +    val {version_id, group, running} = execution_of state;
   4.151      val _ =
   4.152        (singleton o Future.forks)
   4.153          {name = "Document.execution", group = SOME group, deps = [], pri = ~2, interrupts = true}
   4.154 @@ -306,7 +319,7 @@
   4.155                    (fn () =>
   4.156                      iterate_entries (fn (_, opt_exec) => fn () =>
   4.157                        (case opt_exec of
   4.158 -                        SOME exec => if ! running then SOME (Command.exec_run exec) else NONE
   4.159 +                        SOME exec => if ! running then SOME (Command.execute exec) else NONE
   4.160                        | NONE => NONE)) node ()))));
   4.161    in () end;
   4.162  
   4.163 @@ -347,9 +360,9 @@
   4.164            SOME thy => thy
   4.165          | NONE =>
   4.166              Toplevel.end_theory (Position.file_only import)
   4.167 -              (Command.eval_result_state
   4.168 -                (the_default Command.no_eval
   4.169 -                  (get_result (snd (the (AList.lookup (op =) deps import))))))));
   4.170 +              (case get_result (snd (the (AList.lookup (op =) deps import))) of
   4.171 +                NONE => Toplevel.toplevel
   4.172 +              | SOME eval => Command.eval_result_state eval)));
   4.173      val _ = Position.reports (map #2 imports ~~ map Theory.get_markup parents);
   4.174    in Thy_Load.begin_theory master_dir header parents end;
   4.175  
   4.176 @@ -423,9 +436,9 @@
   4.177  
   4.178  in
   4.179  
   4.180 -fun update (old_id: Document_ID.version) (new_id: Document_ID.version) edits state =
   4.181 +fun update old_version_id new_version_id edits state =
   4.182    let
   4.183 -    val old_version = the_version state old_id;
   4.184 +    val old_version = the_version state old_version_id;
   4.185      val new_version = timeit "Document.edit_nodes" (fn () => fold edit_nodes edits old_version);
   4.186  
   4.187      val nodes = nodes_of new_version;
   4.188 @@ -510,7 +523,7 @@
   4.189      val updated_nodes = map_filter #3 updated;
   4.190  
   4.191      val state' = state
   4.192 -      |> define_version new_id (fold put_node updated_nodes new_version);
   4.193 +      |> define_version new_version_id (fold put_node updated_nodes new_version);
   4.194    in (command_execs, state') end;
   4.195  
   4.196  end;
     5.1 --- a/src/Pure/ROOT.ML	Fri Jul 05 22:09:16 2013 +0200
     5.2 +++ b/src/Pure/ROOT.ML	Fri Jul 05 22:58:24 2013 +0200
     5.3 @@ -256,6 +256,7 @@
     5.4  
     5.5  (*toplevel transactions*)
     5.6  use "Isar/proof_node.ML";
     5.7 +use "PIDE/document_id.ML";
     5.8  use "Isar/toplevel.ML";
     5.9  
    5.10  (*theory documents*)
    5.11 @@ -265,7 +266,6 @@
    5.12  use "Isar/outer_syntax.ML";
    5.13  use "General/graph_display.ML";
    5.14  use "Thy/present.ML";
    5.15 -use "PIDE/document_id.ML";
    5.16  use "PIDE/command.ML";
    5.17  use "Thy/thy_load.ML";
    5.18  use "Thy/thy_info.ML";