src/Pure/System/isar.ML
author wenzelm
Tue Apr 09 20:16:52 2013 +0200 (2013-04-09 ago)
changeset 51662 3391a493f39a
parent 50917 9459f59cff09
child 51948 cb5dbc9a06f9
permissions -rw-r--r--
just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
     1 (*  Title:      Pure/System/isar.ML
     2     Author:     Makarius
     3 
     4 Global state of the raw Isar read-eval-print loop.
     5 *)
     6 
     7 signature ISAR =
     8 sig
     9   val init: unit -> unit
    10   val exn: unit -> (exn * string) option
    11   val state: unit -> Toplevel.state
    12   val goal: unit -> {context: Proof.context, facts: thm list, goal: thm}
    13   val print: unit -> unit
    14   val >> : Toplevel.transition -> bool
    15   val >>> : Toplevel.transition list -> unit
    16   val linear_undo: int -> unit
    17   val undo: int -> unit
    18   val kill: unit -> unit
    19   val kill_proof: unit -> unit
    20   val crashes: exn list Synchronized.var
    21   val toplevel_loop: TextIO.instream ->
    22     {init: bool, welcome: bool, sync: bool, secure: bool} -> unit
    23   val loop: unit -> unit
    24   val main: unit -> unit
    25 end;
    26 
    27 structure Isar: ISAR =
    28 struct
    29 
    30 
    31 (** TTY model -- SINGLE-THREADED! **)
    32 
    33 (* the global state *)
    34 
    35 type history = (Toplevel.state * Toplevel.transition) list;
    36   (*previous state, state transition -- regular commands only*)
    37 
    38 local
    39   val global_history = Unsynchronized.ref ([]: history);
    40   val global_state = Unsynchronized.ref Toplevel.toplevel;
    41   val global_exn = Unsynchronized.ref (NONE: (exn * string) option);
    42 in
    43 
    44 fun edit_history count f = NAMED_CRITICAL "Isar" (fn () =>
    45   let
    46     fun edit 0 (st, hist) = (global_history := hist; global_state := st; global_exn := NONE)
    47       | edit n (st, hist) = edit (n - 1) (f st hist);
    48   in edit count (! global_state, ! global_history) end);
    49 
    50 fun state () = ! global_state;
    51 
    52 fun exn () = ! global_exn;
    53 fun set_exn exn =  global_exn := exn;
    54 
    55 end;
    56 
    57 
    58 fun init () = edit_history 1 (K (K (Toplevel.toplevel, [])));
    59 
    60 fun goal () = Proof.goal (Toplevel.proof_of (state ()))
    61   handle Toplevel.UNDEF => error "No goal present";
    62 
    63 fun print () = Toplevel.print_state false (state ());
    64 
    65 
    66 (* history navigation *)
    67 
    68 local
    69 
    70 fun find_and_undo _ [] = error "Undo history exhausted"
    71   | find_and_undo which ((prev, tr) :: hist) =
    72       if which (Toplevel.name_of tr) then (prev, hist) else find_and_undo which hist;
    73 
    74 in
    75 
    76 fun linear_undo n = edit_history n (K (find_and_undo (K true)));
    77 
    78 fun undo n = edit_history n (fn st => fn hist =>
    79   find_and_undo (if Toplevel.is_proof st then K true else Keyword.is_theory) hist);
    80 
    81 fun kill () = edit_history 1 (fn st => fn hist =>
    82   find_and_undo
    83     (if Toplevel.is_proof st then Keyword.is_theory else Keyword.is_theory_begin) hist);
    84 
    85 fun kill_proof () = edit_history 1 (fn st => fn hist =>
    86   if Toplevel.is_proof st then find_and_undo Keyword.is_theory hist
    87   else raise Toplevel.UNDEF);
    88 
    89 end;
    90 
    91 
    92 (* interactive state transformations *)
    93 
    94 fun op >> tr =
    95   (case Toplevel.transition true tr (state ()) of
    96     NONE => false
    97   | SOME (_, SOME exn_info) =>
    98      (set_exn (SOME exn_info);
    99       Toplevel.setmp_thread_position tr
   100         Output.error_msg' (serial (), ML_Compiler.exn_message (Runtime.EXCURSION_FAIL exn_info));
   101       true)
   102   | SOME (st', NONE) =>
   103       let
   104         val name = Toplevel.name_of tr;
   105         val _ = if Keyword.is_theory_begin name then init () else ();
   106         val _ =
   107           if Keyword.is_regular name
   108           then edit_history 1 (fn st => fn hist => (st', (st, tr) :: hist)) else ();
   109       in true end);
   110 
   111 fun op >>> [] = ()
   112   | op >>> (tr :: trs) = if op >> tr then op >>> trs else ();
   113 
   114 
   115 (* toplevel loop -- uninterruptible *)
   116 
   117 val crashes = Synchronized.var "Isar.crashes" ([]: exn list);
   118 
   119 local
   120 
   121 fun protocol_message props output =
   122   (case props of
   123     function :: args =>
   124       if function = Markup.command_timing then
   125         let
   126           val name = the_default "" (Properties.get args Markup.nameN);
   127           val pos = Position.of_properties args;
   128           val timing = Markup.parse_timing_properties args;
   129         in
   130           if Timing.is_relevant timing andalso (! Toplevel.profiling > 0 orelse ! Toplevel.timing)
   131             andalso name <> "" andalso not (Keyword.is_control name)
   132           then tracing ("command " ^ quote name ^ Position.here pos ^ ": " ^ Timing.message timing)
   133           else ()
   134         end
   135       else raise Output.Protocol_Message props
   136   | [] => raise Output.Protocol_Message props);
   137 
   138 fun raw_loop secure src =
   139   let
   140     fun check_secure () =
   141       (if secure then warning "Secure loop -- cannot exit to ML" else (); secure);
   142   in
   143     (case Source.get_single (Source.set_prompt Source.default_prompt src) of
   144       NONE => if secure then quit () else ()
   145     | SOME (tr, src') => if op >> tr orelse check_secure () then raw_loop secure src' else ())
   146     handle exn =>
   147       (Output.error_msg (ML_Compiler.exn_message exn)
   148         handle crash =>
   149           (Synchronized.change crashes (cons crash);
   150             warning "Recovering from Isar toplevel crash -- see also Isar.crashes");
   151         raw_loop secure src)
   152   end;
   153 
   154 in
   155 
   156 fun toplevel_loop in_stream {init = do_init, welcome, sync, secure} =
   157  (Context.set_thread_data NONE;
   158   if do_init then (Options.load_default (); init ()) else ();
   159   Output.Private_Hooks.protocol_message_fn := protocol_message;
   160   if welcome then writeln (Session.welcome ()) else ();
   161   uninterruptible (fn _ => fn () => raw_loop secure (Outer_Syntax.isar in_stream sync)) ());
   162 
   163 end;
   164 
   165 fun loop () =
   166   toplevel_loop TextIO.stdIn
   167     {init = false, welcome = false, sync = false, secure = Secure.is_secure ()};
   168 
   169 fun main () =
   170   toplevel_loop TextIO.stdIn
   171     {init = true, welcome = true, sync = false, secure = Secure.is_secure ()};
   172 
   173 end;