src/Pure/PIDE/command.ML
author wenzelm
Wed Jul 03 17:50:47 2013 +0200 (2013-07-03)
changeset 52511 d5d2093ff224
parent 52510 a4a102237ded
child 52515 0dcadc90550b
permissions -rw-r--r--
allow multiple print functions;
     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 read: span -> Toplevel.transition
    18   val eval: span -> Toplevel.transition ->
    19     Toplevel.state * {malformed: bool} -> {failed: bool} * (Toplevel.state * {malformed: bool})
    20   val print: Toplevel.transition -> Toplevel.state -> (string * unit lazy) list
    21   val print_function: string ->
    22     ({tr: Toplevel.transition, state: Toplevel.state} -> (unit -> unit) option) -> unit
    23 end;
    24 
    25 structure Command: COMMAND =
    26 struct
    27 
    28 (* source *)
    29 
    30 type span = Token.T list;
    31 
    32 val range = Token.position_range_of;
    33 val proper_range = Token.position_range_of o #1 o take_suffix Token.is_improper;
    34 
    35 
    36 (* memo results *)
    37 
    38 datatype 'a expr =
    39   Expr of unit -> 'a |
    40   Result of 'a Exn.result;
    41 
    42 abstype 'a memo = Memo of 'a expr Synchronized.var
    43 with
    44 
    45 fun memo e = Memo (Synchronized.var "Command.memo" (Expr e));
    46 fun memo_value a = Memo (Synchronized.var "Command.memo" (Result (Exn.Res a)));
    47 
    48 fun memo_eval (Memo v) =
    49   (case Synchronized.value v of
    50     Result res => res
    51   | _ =>
    52       Synchronized.guarded_access v
    53         (fn Result res => SOME (res, Result res)
    54           | Expr e =>
    55               let val res = Exn.capture e ();  (*memoing of physical interrupts!*)
    56               in SOME (res, Result res) end))
    57   |> Exn.release;
    58 
    59 fun memo_result (Memo v) =
    60   (case Synchronized.value v of
    61     Result res => Exn.release res
    62   | _ => raise Fail "Unfinished memo result");
    63 
    64 end;
    65 
    66 
    67 (* read *)
    68 
    69 fun read span =
    70   let
    71     val outer_syntax = #2 (Outer_Syntax.get_syntax ());
    72     val command_reports = Outer_Syntax.command_reports outer_syntax;
    73 
    74     val proper_range = Position.set_range (proper_range span);
    75     val pos =
    76       (case find_first Token.is_command span of
    77         SOME tok => Token.position_of tok
    78       | NONE => proper_range);
    79 
    80     val (is_malformed, token_reports) = Thy_Syntax.reports_of_tokens span;
    81     val _ = Position.reports_text (token_reports @ maps command_reports span);
    82   in
    83     if is_malformed then Toplevel.malformed pos "Malformed command syntax"
    84     else
    85       (case Outer_Syntax.read_spans outer_syntax span of
    86         [tr] =>
    87           if Keyword.is_control (Toplevel.name_of tr) then
    88             Toplevel.malformed pos "Illegal control command"
    89           else tr
    90       | [] => Toplevel.ignored (Position.set_range (range span))
    91       | _ => Toplevel.malformed proper_range "Exactly one command expected")
    92       handle ERROR msg => Toplevel.malformed proper_range msg
    93   end;
    94 
    95 
    96 (* eval *)
    97 
    98 local
    99 
   100 fun run int tr st =
   101   if Goal.future_enabled () andalso Keyword.is_diag (Toplevel.name_of tr) then
   102     (Goal.fork_params {name = "Toplevel.diag", pos = Toplevel.pos_of tr, pri = ~1}
   103       (fn () => Toplevel.command_exception int tr st); ([], SOME st))
   104   else Toplevel.command_errors int tr st;
   105 
   106 fun check_cmts span tr st' =
   107   Toplevel.setmp_thread_position tr
   108     (fn () =>
   109       Outer_Syntax.side_comments span |> maps (fn cmt =>
   110         (Thy_Output.check_text (Token.source_position_of cmt) st'; [])
   111           handle exn => ML_Compiler.exn_messages_ids exn)) ();
   112 
   113 fun proof_status tr st =
   114   (case try Toplevel.proof_of st of
   115     SOME prf => Toplevel.status tr (Proof.status_markup prf)
   116   | NONE => ());
   117 
   118 in
   119 
   120 fun eval span tr (st, {malformed}) =
   121   if malformed then
   122     ({failed = true}, (Toplevel.toplevel, {malformed = malformed}))
   123   else
   124     let
   125       val malformed' = Toplevel.is_malformed tr;
   126       val is_init = Toplevel.is_init tr;
   127       val is_proof = Keyword.is_proof (Toplevel.name_of tr);
   128 
   129       val _ = Multithreading.interrupted ();
   130       val _ = Toplevel.status tr Markup.running;
   131       val (errs1, result) = run (is_init orelse is_proof) (Toplevel.set_print false tr) st;
   132       val errs2 = (case result of NONE => [] | SOME st' => check_cmts span tr st');
   133       val errs = errs1 @ errs2;
   134       val _ = Toplevel.status tr Markup.finished;
   135       val _ = List.app (Future.error_msg (Toplevel.pos_of tr)) errs;
   136     in
   137       (case result of
   138         NONE =>
   139           let
   140             val _ = if null errs then Exn.interrupt () else ();
   141             val _ = Toplevel.status tr Markup.failed;
   142           in ({failed = true}, (st, {malformed = malformed'})) end
   143       | SOME st' =>
   144           let
   145             val _ = proof_status tr st';
   146           in ({failed = false}, (st', {malformed = malformed'})) end)
   147     end;
   148 
   149 end;
   150 
   151 
   152 (* print *)
   153 
   154 local
   155 
   156 type print_function =
   157   {tr: Toplevel.transition, state: Toplevel.state} -> (unit -> unit) option;
   158 
   159 val print_functions =
   160   Synchronized.var "Command.print_functions" ([]: (string * print_function) list);
   161 
   162 in
   163 
   164 fun print tr st' =
   165   rev (Synchronized.value print_functions) |> map_filter (fn (name, f) =>
   166     (case f {tr = tr, state = st'} of
   167       SOME pr => SOME (name, (Lazy.lazy o Toplevel.setmp_thread_position tr) pr)
   168     | NONE => NONE));
   169 
   170 fun print_function name f =
   171   Synchronized.change print_functions (fn funs =>
   172    (if not (AList.defined (op =) funs name) then ()
   173     else warning ("Redefining command print function: " ^ quote name);
   174     AList.update (op =) (name, f) funs));
   175 
   176 end;
   177 
   178 val _ = print_function "print_state" (fn {tr, state} =>
   179   let
   180     val is_init = Toplevel.is_init tr;
   181     val is_proof = Keyword.is_proof (Toplevel.name_of tr);
   182     val do_print =
   183       not is_init andalso
   184         (Toplevel.print_of tr orelse (is_proof andalso Toplevel.is_proof state));
   185   in if do_print then SOME (fn () => Toplevel.print_state false state) else NONE end);
   186 
   187 end;
   188