src/Pure/PIDE/document.ML
changeset 47336 bed4b2738d8a
parent 47335 693276dcc512
child 47339 79bd24497ffd
     1.1 --- a/src/Pure/PIDE/document.ML	Wed Apr 04 14:00:47 2012 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Wed Apr 04 14:19:47 2012 +0200
     1.3 @@ -63,8 +63,7 @@
     1.4  structure Entries = Linear_Set(type key = command_id val ord = int_ord);
     1.5  
     1.6  type exec = exec_id * (Toplevel.state * unit lazy) lazy;  (*eval/print process*)
     1.7 -val no_print = Lazy.value ();
     1.8 -val no_exec = (no_id, Lazy.value (Toplevel.toplevel, no_print));
     1.9 +val no_exec = (no_id, Lazy.value (Toplevel.toplevel, Lazy.value ()));
    1.10  
    1.11  abstype node = Node of
    1.12   {touched: bool,
    1.13 @@ -276,18 +275,10 @@
    1.14  
    1.15  (* commands *)
    1.16  
    1.17 -fun parse_command id text =
    1.18 -  Position.setmp_thread_data (Position.id_only id)
    1.19 -    (fn () =>
    1.20 -      let
    1.21 -        val toks = Thy_Syntax.parse_tokens (#1 (Outer_Syntax.get_syntax ())) (Position.id id) text;
    1.22 -        val _ = Output.status (Markup.markup_only Isabelle_Markup.parsed);
    1.23 -      in toks end) ();
    1.24 -
    1.25  fun define_command (id: command_id) name text =
    1.26    map_state (fn (versions, commands, execution) =>
    1.27      let
    1.28 -      val span = Lazy.lazy (fn () => parse_command (print_id id) text);
    1.29 +      val span = Lazy.lazy (fn () => Command.parse_command (print_id id) text);
    1.30        val commands' =
    1.31          Inttab.update_new (id, (name, span)) commands
    1.32            handle Inttab.DUP dup => err_dup "command" dup;
    1.33 @@ -306,62 +297,6 @@
    1.34  end;
    1.35  
    1.36  
    1.37 -(* toplevel transactions *)
    1.38 -
    1.39 -local
    1.40 -
    1.41 -fun run int tr st =
    1.42 -  (case Toplevel.transition int tr st of
    1.43 -    SOME (st', NONE) => ([], SOME st')
    1.44 -  | SOME (_, SOME (exn, _)) => (ML_Compiler.exn_messages exn, NONE)
    1.45 -  | NONE => ([(serial (), ML_Compiler.exn_message Runtime.TERMINATE)], NONE));
    1.46 -
    1.47 -fun timing tr t =
    1.48 -  if Timing.is_relevant t then Toplevel.status tr (Isabelle_Markup.timing t) else ();
    1.49 -
    1.50 -fun proof_status tr st =
    1.51 -  (case try Toplevel.proof_of st of
    1.52 -    SOME prf => Toplevel.status tr (Proof.status_markup prf)
    1.53 -  | NONE => ());
    1.54 -
    1.55 -fun print_state tr st =
    1.56 -  (Lazy.lazy o Toplevel.setmp_thread_position tr)
    1.57 -    (fn () => Toplevel.print_state false st);
    1.58 -
    1.59 -in
    1.60 -
    1.61 -fun run_command tr st =
    1.62 -  let
    1.63 -    val is_init = Toplevel.is_init tr;
    1.64 -    val is_proof = Keyword.is_proof (Toplevel.name_of tr);
    1.65 -
    1.66 -    val _ = Multithreading.interrupted ();
    1.67 -    val _ = Toplevel.status tr Isabelle_Markup.forked;
    1.68 -    val start = Timing.start ();
    1.69 -    val (errs, result) = run (is_init orelse is_proof) (Toplevel.set_print false tr) st;
    1.70 -    val _ = timing tr (Timing.result start);
    1.71 -    val _ = Toplevel.status tr Isabelle_Markup.joined;
    1.72 -    val _ = List.app (Toplevel.error_msg tr) errs;
    1.73 -  in
    1.74 -    (case result of
    1.75 -      NONE =>
    1.76 -        let
    1.77 -          val _ = if null errs then Exn.interrupt () else ();
    1.78 -          val _ = Toplevel.status tr Isabelle_Markup.failed;
    1.79 -        in (st, no_print) end
    1.80 -    | SOME st' =>
    1.81 -        let
    1.82 -          val _ = Toplevel.status tr Isabelle_Markup.finished;
    1.83 -          val _ = proof_status tr st';
    1.84 -          val do_print =
    1.85 -            not is_init andalso
    1.86 -              (Toplevel.print_of tr orelse (is_proof andalso Toplevel.is_proof st'));
    1.87 -        in (st', if do_print then print_state tr st' else no_print) end)
    1.88 -  end;
    1.89 -
    1.90 -end;
    1.91 -
    1.92 -
    1.93  
    1.94  (** update **)
    1.95  
    1.96 @@ -454,7 +389,8 @@
    1.97              #1 (Outer_Syntax.read_span (#2 (Outer_Syntax.get_syntax ())) span)
    1.98              |> modify_init
    1.99              |> Toplevel.put_id exec_id'_string);
   1.100 -      val exec' = snd (snd command_exec) |> Lazy.map (fn (st, _) => run_command (tr ()) st);
   1.101 +      val exec' =
   1.102 +        snd (snd command_exec) |> Lazy.map (fn (st, _) => Command.run_command (tr ()) st);
   1.103        val command_exec' = (command_id', (exec_id', exec'));
   1.104      in SOME (command_exec' :: execs, command_exec', init') end;
   1.105