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