src/Pure/PIDE/command.ML
author wenzelm
Wed Apr 04 14:19:47 2012 +0200 (2012-04-04 ago)
changeset 47336 bed4b2738d8a
child 47341 00f6279bb67a
permissions -rw-r--r--
separate module for prover command execution;
wenzelm@47336
     1
(*  Title:      Pure/PIDE/command.ML
wenzelm@47336
     2
    Author:     Makarius
wenzelm@47336
     3
wenzelm@47336
     4
Prover command execution.
wenzelm@47336
     5
*)
wenzelm@47336
     6
wenzelm@47336
     7
signature COMMAND =
wenzelm@47336
     8
sig
wenzelm@47336
     9
  val parse_command: string -> string -> Token.T list
wenzelm@47336
    10
  val run_command: Toplevel.transition -> Toplevel.state -> Toplevel.state * unit lazy
wenzelm@47336
    11
end;
wenzelm@47336
    12
wenzelm@47336
    13
structure Command: COMMAND =
wenzelm@47336
    14
struct
wenzelm@47336
    15
wenzelm@47336
    16
(* parse *)
wenzelm@47336
    17
wenzelm@47336
    18
fun parse_command id text =
wenzelm@47336
    19
  Position.setmp_thread_data (Position.id_only id)
wenzelm@47336
    20
    (fn () =>
wenzelm@47336
    21
      let
wenzelm@47336
    22
        val toks = Thy_Syntax.parse_tokens (#1 (Outer_Syntax.get_syntax ())) (Position.id id) text;
wenzelm@47336
    23
        val _ = Output.status (Markup.markup_only Isabelle_Markup.parsed);
wenzelm@47336
    24
      in toks end) ();
wenzelm@47336
    25
wenzelm@47336
    26
wenzelm@47336
    27
(* run *)
wenzelm@47336
    28
wenzelm@47336
    29
local
wenzelm@47336
    30
wenzelm@47336
    31
fun run int tr st =
wenzelm@47336
    32
  (case Toplevel.transition int tr st of
wenzelm@47336
    33
    SOME (st', NONE) => ([], SOME st')
wenzelm@47336
    34
  | SOME (_, SOME (exn, _)) => (ML_Compiler.exn_messages exn, NONE)
wenzelm@47336
    35
  | NONE => ([(serial (), ML_Compiler.exn_message Runtime.TERMINATE)], NONE));
wenzelm@47336
    36
wenzelm@47336
    37
fun timing tr t =
wenzelm@47336
    38
  if Timing.is_relevant t then Toplevel.status tr (Isabelle_Markup.timing t) else ();
wenzelm@47336
    39
wenzelm@47336
    40
fun proof_status tr st =
wenzelm@47336
    41
  (case try Toplevel.proof_of st of
wenzelm@47336
    42
    SOME prf => Toplevel.status tr (Proof.status_markup prf)
wenzelm@47336
    43
  | NONE => ());
wenzelm@47336
    44
wenzelm@47336
    45
val no_print = Lazy.value ();
wenzelm@47336
    46
wenzelm@47336
    47
fun print_state tr st =
wenzelm@47336
    48
  (Lazy.lazy o Toplevel.setmp_thread_position tr)
wenzelm@47336
    49
    (fn () => Toplevel.print_state false st);
wenzelm@47336
    50
wenzelm@47336
    51
in
wenzelm@47336
    52
wenzelm@47336
    53
fun run_command tr st =
wenzelm@47336
    54
  let
wenzelm@47336
    55
    val is_init = Toplevel.is_init tr;
wenzelm@47336
    56
    val is_proof = Keyword.is_proof (Toplevel.name_of tr);
wenzelm@47336
    57
wenzelm@47336
    58
    val _ = Multithreading.interrupted ();
wenzelm@47336
    59
    val _ = Toplevel.status tr Isabelle_Markup.forked;
wenzelm@47336
    60
    val start = Timing.start ();
wenzelm@47336
    61
    val (errs, result) = run (is_init orelse is_proof) (Toplevel.set_print false tr) st;
wenzelm@47336
    62
    val _ = timing tr (Timing.result start);
wenzelm@47336
    63
    val _ = Toplevel.status tr Isabelle_Markup.joined;
wenzelm@47336
    64
    val _ = List.app (Toplevel.error_msg tr) errs;
wenzelm@47336
    65
  in
wenzelm@47336
    66
    (case result of
wenzelm@47336
    67
      NONE =>
wenzelm@47336
    68
        let
wenzelm@47336
    69
          val _ = if null errs then Exn.interrupt () else ();
wenzelm@47336
    70
          val _ = Toplevel.status tr Isabelle_Markup.failed;
wenzelm@47336
    71
        in (st, no_print) end
wenzelm@47336
    72
    | SOME st' =>
wenzelm@47336
    73
        let
wenzelm@47336
    74
          val _ = Toplevel.status tr Isabelle_Markup.finished;
wenzelm@47336
    75
          val _ = proof_status tr st';
wenzelm@47336
    76
          val do_print =
wenzelm@47336
    77
            not is_init andalso
wenzelm@47336
    78
              (Toplevel.print_of tr orelse (is_proof andalso Toplevel.is_proof st'));
wenzelm@47336
    79
        in (st', if do_print then print_state tr st' else no_print) end)
wenzelm@47336
    80
  end;
wenzelm@47336
    81
wenzelm@47336
    82
end;
wenzelm@47336
    83
wenzelm@47336
    84
end;
wenzelm@47336
    85