src/Pure/PIDE/command.ML
author wenzelm
Wed Jul 03 16:19:57 2013 +0200 (2013-07-03 ago)
changeset 52509 2193d2c7f586
parent 51605 eca8acb42e4a
child 52510 a4a102237ded
permissions -rw-r--r--
tuned signature;
     1 (*  Title:      Pure/PIDE/command.ML
     2     Author:     Makarius
     3 
     4 Prover command execution.
     5 *)
     6 
     7 signature COMMAND =
     8 sig
     9   type span = Token.T list
    10   val range: span -> Position.range
    11   val proper_range: span -> Position.range
    12   type 'a memo
    13   val memo: (unit -> 'a) -> 'a memo
    14   val memo_value: 'a -> 'a memo
    15   val memo_eval: 'a memo -> 'a
    16   val memo_result: 'a memo -> 'a
    17   val eval: span -> Toplevel.transition ->
    18     Toplevel.state * {malformed: bool} -> {failed: bool} * (Toplevel.state * {malformed: bool})
    19   val no_print: unit lazy
    20   val print: Toplevel.transition -> Toplevel.state -> unit lazy
    21 end;
    22 
    23 structure Command: COMMAND =
    24 struct
    25 
    26 (* source *)
    27 
    28 type span = Token.T list;
    29 
    30 val range = Token.position_range_of;
    31 val proper_range = Token.position_range_of o #1 o take_suffix Token.is_improper;
    32 
    33 
    34 (* memo results *)
    35 
    36 datatype 'a expr =
    37   Expr of unit -> 'a |
    38   Result of 'a Exn.result;
    39 
    40 abstype 'a memo = Memo of 'a expr Synchronized.var
    41 with
    42 
    43 fun memo e = Memo (Synchronized.var "Command.memo" (Expr e));
    44 fun memo_value a = Memo (Synchronized.var "Command.memo" (Result (Exn.Res a)));
    45 
    46 fun memo_eval (Memo v) =
    47   (case Synchronized.value v of
    48     Result res => res
    49   | _ =>
    50       Synchronized.guarded_access v
    51         (fn Result res => SOME (res, Result res)
    52           | Expr e =>
    53               let val res = Exn.capture e ();  (*memoing of physical interrupts!*)
    54               in SOME (res, Result res) end))
    55   |> Exn.release;
    56 
    57 fun memo_result (Memo v) =
    58   (case Synchronized.value v of
    59     Result res => Exn.release res
    60   | _ => raise Fail "Unfinished memo result");
    61 
    62 end;
    63 
    64 
    65 (* side-comments *)
    66 
    67 local
    68 
    69 fun cmts (t1 :: t2 :: toks) =
    70       if Token.keyword_with (fn s => s = "--") t1 then t2 :: cmts toks
    71       else cmts (t2 :: toks)
    72   | cmts _ = [];
    73 
    74 val span_cmts = filter Token.is_proper #> cmts;
    75 
    76 in
    77 
    78 fun check_cmts span tr st' =
    79   Toplevel.setmp_thread_position tr
    80     (fn () =>
    81       span_cmts span |> maps (fn cmt =>
    82         (Thy_Output.check_text (Token.source_position_of cmt) st'; [])
    83           handle exn => ML_Compiler.exn_messages_ids exn)) ();
    84 
    85 end;
    86 
    87 
    88 (* eval *)
    89 
    90 local
    91 
    92 fun run int tr st =
    93   if Goal.future_enabled () andalso Keyword.is_diag (Toplevel.name_of tr) then
    94     (Goal.fork_params {name = "Toplevel.diag", pos = Toplevel.pos_of tr, pri = ~1}
    95       (fn () => Toplevel.command_exception int tr st); ([], SOME st))
    96   else Toplevel.command_errors int tr st;
    97 
    98 fun proof_status tr st =
    99   (case try Toplevel.proof_of st of
   100     SOME prf => Toplevel.status tr (Proof.status_markup prf)
   101   | NONE => ());
   102 
   103 in
   104 
   105 fun eval span tr (st, {malformed}) =
   106   if malformed then
   107     ({failed = true}, (Toplevel.toplevel, {malformed = malformed}))
   108   else
   109     let
   110       val malformed' = Toplevel.is_malformed tr;
   111       val is_init = Toplevel.is_init tr;
   112       val is_proof = Keyword.is_proof (Toplevel.name_of tr);
   113 
   114       val _ = Multithreading.interrupted ();
   115       val _ = Toplevel.status tr Markup.running;
   116       val (errs1, result) = run (is_init orelse is_proof) (Toplevel.set_print false tr) st;
   117       val errs2 = (case result of NONE => [] | SOME st' => check_cmts span tr st');
   118       val errs = errs1 @ errs2;
   119       val _ = Toplevel.status tr Markup.finished;
   120       val _ = List.app (Future.error_msg (Toplevel.pos_of tr)) errs;
   121     in
   122       (case result of
   123         NONE =>
   124           let
   125             val _ = if null errs then Exn.interrupt () else ();
   126             val _ = Toplevel.status tr Markup.failed;
   127           in ({failed = true}, (st, {malformed = malformed'})) end
   128       | SOME st' =>
   129           let
   130             val _ = proof_status tr st';
   131           in ({failed = false}, (st', {malformed = malformed'})) end)
   132     end;
   133 
   134 end;
   135 
   136 
   137 (* print *)
   138 
   139 val no_print = Lazy.value ();
   140 
   141 fun print tr st' =
   142   let
   143     val is_init = Toplevel.is_init tr;
   144     val is_proof = Keyword.is_proof (Toplevel.name_of tr);
   145     val do_print =
   146       not is_init andalso
   147         (Toplevel.print_of tr orelse (is_proof andalso Toplevel.is_proof st'));
   148   in
   149     if do_print then
   150       (Lazy.lazy o Toplevel.setmp_thread_position tr)
   151         (fn () => Toplevel.print_state false st')
   152     else no_print
   153   end;
   154 
   155 end;
   156