tuned signature;
authorwenzelm
Fri Jul 05 18:37:44 2013 +0200 (2013-07-05 ago)
changeset 52534341ae9cd4743
parent 52533 a95440dcd59c
child 52535 b7badd371e4d
tuned signature;
tuned;
src/Pure/PIDE/command.ML
src/Pure/PIDE/document.ML
src/Pure/Thy/thy_load.ML
     1.1 --- a/src/Pure/PIDE/command.ML	Fri Jul 05 17:09:28 2013 +0200
     1.2 +++ b/src/Pure/PIDE/command.ML	Fri Jul 05 18:37:44 2013 +0200
     1.3 @@ -1,36 +1,26 @@
     1.4  (*  Title:      Pure/PIDE/command.ML
     1.5      Author:     Makarius
     1.6  
     1.7 -Prover command execution.
     1.8 +Prover command execution: read -- eval -- print.
     1.9  *)
    1.10  
    1.11  signature COMMAND =
    1.12  sig
    1.13 -  type span = Token.T list
    1.14 -  val range: span -> Position.range
    1.15 -  val proper_range: span -> Position.range
    1.16 -  type 'a memo
    1.17 -  val memo: (unit -> 'a) -> 'a memo
    1.18 -  val memo_value: 'a -> 'a memo
    1.19 -  val memo_eval: 'a memo -> 'a
    1.20 -  val memo_fork: Future.params -> 'a memo -> unit
    1.21 -  val memo_result: 'a memo -> 'a
    1.22 -  val memo_stable: 'a memo -> bool
    1.23 -  val read: span -> Toplevel.transition
    1.24 -  type eval_state =
    1.25 -    {failed: bool, malformed: bool, command: Toplevel.transition, state: Toplevel.state}
    1.26 -  type eval = {exec_id: Document_ID.exec, eval: eval_state memo}
    1.27 +  type span
    1.28 +  type eval_process
    1.29 +  type eval = {exec_id: Document_ID.exec, eval_process: eval_process}
    1.30 +  type print_process
    1.31 +  type print = {name: string, pri: int, exec_id: Document_ID.exec, print_process: print_process}
    1.32 +  type exec = eval * print list
    1.33 +  val read: (unit -> theory) -> span -> Toplevel.transition
    1.34    val no_eval: eval
    1.35 -  val eval_result: eval -> eval_state
    1.36 -  val eval: span -> Toplevel.transition -> eval_state -> eval_state
    1.37 +  val eval_result_state: eval -> Toplevel.state
    1.38 +  val eval: (unit -> theory) -> span -> eval -> eval
    1.39 +  val print: string -> eval -> print list
    1.40    type print_fn = Toplevel.transition -> Toplevel.state -> unit
    1.41 -  type print = {name: string, pri: int, exec_id: Document_ID.exec, print: unit memo}
    1.42 -  val print: string -> eval -> print list
    1.43    val print_function: {name: string, pri: int} -> (string -> print_fn option) -> unit
    1.44 -  type exec = eval * print list
    1.45    val no_exec: exec
    1.46    val exec_ids: exec -> Document_ID.exec list
    1.47 -  val exec_result: exec -> eval_state
    1.48    val exec_run: exec -> unit
    1.49    val stable_eval: eval -> bool
    1.50    val stable_print: print -> bool
    1.51 @@ -39,15 +29,7 @@
    1.52  structure Command: COMMAND =
    1.53  struct
    1.54  
    1.55 -(* source *)
    1.56 -
    1.57 -type span = Token.T list;
    1.58 -
    1.59 -val range = Token.position_range_of;
    1.60 -val proper_range = Token.position_range_of o #1 o take_suffix Token.is_improper;
    1.61 -
    1.62 -
    1.63 -(* memo results *)
    1.64 +(** memo results -- including physical interrupts! **)
    1.65  
    1.66  datatype 'a expr =
    1.67    Expr of unit -> 'a |
    1.68 @@ -66,7 +48,7 @@
    1.69        Synchronized.guarded_access v
    1.70          (fn Result res => SOME (res, Result res)
    1.71            | Expr e =>
    1.72 -              let val res = Exn.capture e ();  (*memoing of physical interrupts!*)
    1.73 +              let val res = Exn.capture e ();  (*sic!*)
    1.74                in SOME (res, Result res) end))
    1.75    |> Exn.release;
    1.76  
    1.77 @@ -88,16 +70,29 @@
    1.78  end;
    1.79  
    1.80  
    1.81 -(** main phases: read -- eval -- print **)
    1.82 +
    1.83 +(** main phases **)
    1.84 +
    1.85 +type span = Token.T list
    1.86 +
    1.87 +type eval_state =
    1.88 +  {failed: bool, malformed: bool, command: Toplevel.transition, state: Toplevel.state};
    1.89 +type eval_process = eval_state memo;
    1.90 +type eval = {exec_id: Document_ID.exec, eval_process: eval_process};
    1.91 +
    1.92 +type print_process = unit memo;
    1.93 +type print = {name: string, pri: int, exec_id: Document_ID.exec, print_process: print_process};
    1.94 +
    1.95  
    1.96  (* read *)
    1.97  
    1.98 -fun read span =
    1.99 +fun read init span =
   1.100    let
   1.101      val outer_syntax = #2 (Outer_Syntax.get_syntax ());
   1.102      val command_reports = Outer_Syntax.command_reports outer_syntax;
   1.103  
   1.104 -    val proper_range = Position.set_range (proper_range span);
   1.105 +    val proper_range =
   1.106 +      Position.set_range (Token.position_range_of (#1 (take_suffix Token.is_improper span)));
   1.107      val pos =
   1.108        (case find_first Token.is_command span of
   1.109          SOME tok => Token.position_of tok
   1.110 @@ -112,8 +107,8 @@
   1.111          [tr] =>
   1.112            if Keyword.is_control (Toplevel.name_of tr) then
   1.113              Toplevel.malformed pos "Illegal control command"
   1.114 -          else tr
   1.115 -      | [] => Toplevel.ignored (Position.set_range (range span))
   1.116 +          else Toplevel.modify_init init tr
   1.117 +      | [] => Toplevel.ignored (Position.set_range (Token.position_range_of span))
   1.118        | _ => Toplevel.malformed proper_range "Exactly one command expected")
   1.119        handle ERROR msg => Toplevel.malformed proper_range msg
   1.120    end;
   1.121 @@ -121,15 +116,13 @@
   1.122  
   1.123  (* eval *)
   1.124  
   1.125 -type eval_state =
   1.126 -  {failed: bool, malformed: bool, command: Toplevel.transition, state: Toplevel.state};
   1.127  val no_eval_state: eval_state =
   1.128    {failed = false, malformed = false, command = Toplevel.empty, state = Toplevel.toplevel};
   1.129  
   1.130 -type eval = {exec_id: Document_ID.exec, eval: eval_state memo};
   1.131 +val no_eval: eval = {exec_id = Document_ID.none, eval_process = memo_value no_eval_state};
   1.132  
   1.133 -val no_eval: eval = {exec_id = Document_ID.none, eval = memo_value no_eval_state};
   1.134 -fun eval_result ({eval, ...}: eval) = memo_result eval;
   1.135 +fun eval_result ({eval_process, ...}: eval) = memo_result eval_process;
   1.136 +val eval_result_state = #state o eval_result;
   1.137  
   1.138  local
   1.139  
   1.140 @@ -151,9 +144,7 @@
   1.141      SOME prf => Toplevel.status tr (Proof.status_markup prf)
   1.142    | NONE => ());
   1.143  
   1.144 -in
   1.145 -
   1.146 -fun eval span tr ({malformed, state = st, ...}: eval_state) =
   1.147 +fun eval_state span tr ({malformed, state = st, ...}: eval_state) =
   1.148    if malformed then
   1.149      {failed = true, malformed = malformed, command = tr, state = Toplevel.toplevel}
   1.150    else
   1.151 @@ -182,12 +173,24 @@
   1.152            in {failed = false, malformed = malformed', command = tr, state = st'} end)
   1.153      end;
   1.154  
   1.155 +in
   1.156 +
   1.157 +fun eval init span eval0 =
   1.158 +  let
   1.159 +    val exec_id = Document_ID.make ();
   1.160 +    fun process () =
   1.161 +      let
   1.162 +        val tr =
   1.163 +          Position.setmp_thread_data (Position.id_only (Document_ID.print exec_id))
   1.164 +            (fn () => read init span |> Toplevel.put_id exec_id) ();
   1.165 +      in eval_state span tr (eval_result eval0) end;
   1.166 +  in {exec_id = exec_id, eval_process = memo process} end;
   1.167 +
   1.168  end;
   1.169  
   1.170  
   1.171  (* print *)
   1.172  
   1.173 -type print = {name: string, pri: int, exec_id: Document_ID.exec, print: unit memo};
   1.174  type print_fn = Toplevel.transition -> Toplevel.state -> unit;
   1.175  
   1.176  local
   1.177 @@ -211,21 +214,21 @@
   1.178      | Exn.Res (SOME print_fn) =>
   1.179          let
   1.180            val exec_id = Document_ID.make ();
   1.181 -          fun body () =
   1.182 +          fun process () =
   1.183              let
   1.184                val {failed, command, state = st', ...} = eval_result eval;
   1.185                val tr = Toplevel.put_id exec_id command;
   1.186              in if failed then () else print_error tr (fn () => print_fn tr st') () end;
   1.187 -        in SOME {name = name, pri = pri, exec_id = exec_id, print = memo body} end
   1.188 +        in SOME {name = name, pri = pri, exec_id = exec_id, print_process = memo process} end
   1.189      | Exn.Exn exn =>
   1.190          let
   1.191            val exec_id = Document_ID.make ();
   1.192 -          fun body () =
   1.193 +          fun process () =
   1.194              let
   1.195                val {command, ...} = eval_result eval;
   1.196                val tr = Toplevel.put_id exec_id command;
   1.197              in output_error tr exn end;
   1.198 -        in SOME {name = name, pri = pri, exec_id = exec_id, print = memo body} end));
   1.199 +        in SOME {name = name, pri = pri, exec_id = exec_id, print_process = memo process} end));
   1.200  
   1.201  fun print_function {name, pri} f =
   1.202    Synchronized.change print_functions (fn funs =>
   1.203 @@ -256,12 +259,10 @@
   1.204  
   1.205  fun exec_ids (({exec_id, ...}, prints): exec) = exec_id :: map #exec_id prints;
   1.206  
   1.207 -fun exec_result (({eval, ...}, _): exec) = memo_result eval;
   1.208 -
   1.209 -fun exec_run (({eval, ...}, prints): exec) =
   1.210 - (memo_eval eval;
   1.211 -  prints |> List.app (fn {name, pri, print, ...} =>
   1.212 -    memo_fork {name = name, group = NONE, deps = [], pri = pri, interrupts = true} print));
   1.213 +fun exec_run (({eval_process, ...}, prints): exec) =
   1.214 + (memo_eval eval_process;
   1.215 +  prints |> List.app (fn {name, pri, print_process, ...} =>
   1.216 +    memo_fork {name = name, group = NONE, deps = [], pri = pri, interrupts = true} print_process));
   1.217  
   1.218  
   1.219  (* stable situations after cancellation *)
   1.220 @@ -269,11 +270,11 @@
   1.221  fun stable_goals exec_id =
   1.222    not (Par_Exn.is_interrupted (Future.join_results (Goal.peek_futures exec_id)));
   1.223  
   1.224 -fun stable_eval ({exec_id, eval}: eval) =
   1.225 -  stable_goals exec_id andalso memo_stable eval;
   1.226 +fun stable_eval ({exec_id, eval_process}: eval) =
   1.227 +  stable_goals exec_id andalso memo_stable eval_process;
   1.228  
   1.229 -fun stable_print ({exec_id, print, ...}: print) =
   1.230 -  stable_goals exec_id andalso memo_stable print;
   1.231 +fun stable_print ({exec_id, print_process, ...}: print) =
   1.232 +  stable_goals exec_id andalso memo_stable print_process;
   1.233  
   1.234  end;
   1.235  
     2.1 --- a/src/Pure/PIDE/document.ML	Fri Jul 05 17:09:28 2013 +0200
     2.2 +++ b/src/Pure/PIDE/document.ML	Fri Jul 05 18:37:44 2013 +0200
     2.3 @@ -109,8 +109,8 @@
     2.4    map_node (fn (header, perspective, entries, _) => (header, perspective, entries, result));
     2.5  
     2.6  fun finished_theory node =
     2.7 -  (case Exn.capture (Command.eval_result o the) (get_result node) of
     2.8 -    Exn.Res {state = st, ...} => can (Toplevel.end_theory Position.none) st
     2.9 +  (case Exn.capture (Command.eval_result_state o the) (get_result node) of
    2.10 +    Exn.Res st => can (Toplevel.end_theory Position.none) st
    2.11    | _ => false);
    2.12  
    2.13  fun get_node nodes name = String_Graph.get_node nodes name
    2.14 @@ -347,10 +347,9 @@
    2.15            SOME thy => thy
    2.16          | NONE =>
    2.17              Toplevel.end_theory (Position.file_only import)
    2.18 -              (#state
    2.19 -                (Command.eval_result
    2.20 -                  (the_default Command.no_eval
    2.21 -                    (get_result (snd (the (AList.lookup (op =) deps import)))))))));
    2.22 +              (Command.eval_result_state
    2.23 +                (the_default Command.no_eval
    2.24 +                  (get_result (snd (the (AList.lookup (op =) deps import))))))));
    2.25      val _ = Position.reports (map #2 imports ~~ map Theory.get_markup parents);
    2.26    in Thy_Load.begin_theory master_dir header parents end;
    2.27  
    2.28 @@ -391,31 +390,16 @@
    2.29      else (common, flags)
    2.30    end;
    2.31  
    2.32 +fun illegal_init _ = error "Illegal theory header after end of theory";
    2.33 +
    2.34  fun new_exec state proper_init command_visible command_id' (execs, command_exec, init) =
    2.35    if not proper_init andalso is_none init then NONE
    2.36    else
    2.37      let
    2.38 +      val (_, (eval, _)) = command_exec;
    2.39        val (command_name, span) = the_command state command_id' ||> Lazy.force;
    2.40 -
    2.41 -      fun illegal_init _ = error "Illegal theory header after end of theory";
    2.42 -      val (modify_init, init') =
    2.43 -        if Keyword.is_theory_begin command_name then
    2.44 -          (Toplevel.modify_init (fn () => the_default illegal_init init span), NONE)
    2.45 -        else (I, init);
    2.46 -
    2.47 -      val exec_id' = Document_ID.make ();
    2.48 -      val eval_body' =
    2.49 -        Command.memo (fn () =>
    2.50 -          let
    2.51 -            val eval_state = Command.exec_result (snd command_exec);
    2.52 -            val tr =
    2.53 -              Position.setmp_thread_data (Position.id_only (Document_ID.print exec_id'))
    2.54 -                (fn () =>
    2.55 -                  Command.read span
    2.56 -                  |> modify_init
    2.57 -                  |> Toplevel.put_id exec_id') ();
    2.58 -          in Command.eval span tr eval_state end);
    2.59 -      val eval' = {exec_id = exec_id', eval = eval_body'};
    2.60 +      val init' = if Keyword.is_theory_begin command_name then NONE else init;
    2.61 +      val eval' = Command.eval (fn () => the_default illegal_init init span) span eval;
    2.62        val prints' = if command_visible then Command.print command_name eval' else [];
    2.63        val command_exec' = (command_id', (eval', prints'));
    2.64      in SOME (command_exec' :: execs, command_exec', init') end;
     3.1 --- a/src/Pure/Thy/thy_load.ML	Fri Jul 05 17:09:28 2013 +0200
     3.2 +++ b/src/Pure/Thy/thy_load.ML	Fri Jul 05 18:37:44 2013 +0200
     3.3 @@ -217,8 +217,7 @@
     3.4    let
     3.5      fun prepare_span span =
     3.6        Thy_Syntax.span_content span
     3.7 -      |> Command.read
     3.8 -      |> Toplevel.modify_init init
     3.9 +      |> Command.read init
    3.10        |> (fn tr => Toplevel.put_timing (last_timing tr) tr);
    3.11  
    3.12      fun element_result span_elem (st, _) =