src/Pure/System/isar.ML
author wenzelm
Tue Sep 01 21:40:10 2009 +0200 (2009-09-01 ago)
changeset 32486 67972a7f85b7
parent 31478 5e412e4c6546
child 32738 15bb09ca0378
permissions -rw-r--r--
removed old Isar document model;
wenzelm@30175
     1
(*  Title:      Pure/System/isar.ML
wenzelm@26605
     2
    Author:     Makarius
wenzelm@26605
     3
wenzelm@26605
     4
The global Isabelle/Isar state and main 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@26605
    12
  val context: unit -> Proof.context
wenzelm@26605
    13
  val goal: unit -> thm
wenzelm@27533
    14
  val print: unit -> unit
wenzelm@26605
    15
  val >> : Toplevel.transition -> bool
wenzelm@26605
    16
  val >>> : Toplevel.transition list -> unit
wenzelm@27529
    17
  val linear_undo: int -> unit
wenzelm@27524
    18
  val undo: int -> unit
wenzelm@27530
    19
  val kill: unit -> unit
wenzelm@27530
    20
  val kill_proof: unit -> unit
wenzelm@26605
    21
  val crashes: exn list ref
wenzelm@26643
    22
  val toplevel_loop: {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@29348
    39
  val global_history = ref ([]: history);
wenzelm@29348
    40
  val global_state = ref Toplevel.toplevel;
wenzelm@29348
    41
  val global_exn = 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@29348
    50
fun state () = NAMED_CRITICAL "Isar" (fn () => ! global_state);
wenzelm@29348
    51
fun set_state state = NAMED_CRITICAL "Isar" (fn () => global_state := state);
wenzelm@29348
    52
wenzelm@29348
    53
fun exn () = NAMED_CRITICAL "Isar" (fn () => ! global_exn);
wenzelm@29348
    54
fun set_exn exn =  NAMED_CRITICAL "Isar" (fn () => global_exn := exn);
wenzelm@29348
    55
wenzelm@29348
    56
end;
wenzelm@29348
    57
wenzelm@29348
    58
wenzelm@29348
    59
fun init () = edit_history 1 (K (K (Toplevel.toplevel, [])));
wenzelm@29348
    60
wenzelm@29348
    61
fun context () = Toplevel.context_of (state ())
wenzelm@29348
    62
  handle Toplevel.UNDEF => error "Unknown context";
wenzelm@29348
    63
wenzelm@29348
    64
fun goal () = #2 (#2 (Proof.get_goal (Toplevel.proof_of (state ()))))
wenzelm@29348
    65
  handle Toplevel.UNDEF => error "No goal present";
wenzelm@29348
    66
wenzelm@29348
    67
fun print () = Toplevel.print_state false (state ());
wenzelm@29348
    68
wenzelm@29348
    69
wenzelm@29348
    70
(* history navigation *)
wenzelm@29348
    71
wenzelm@29348
    72
local
wenzelm@29348
    73
wenzelm@29348
    74
fun find_and_undo _ [] = error "Undo history exhausted"
wenzelm@29348
    75
  | find_and_undo which ((prev, tr) :: hist) =
wenzelm@29348
    76
      ((case Toplevel.init_of tr of SOME name => ThyInfo.kill_thy name | NONE => ());
wenzelm@29348
    77
        if which (Toplevel.name_of tr) then (prev, hist) else find_and_undo which hist);
wenzelm@29348
    78
wenzelm@29348
    79
in
wenzelm@29348
    80
wenzelm@29348
    81
fun linear_undo n = edit_history n (K (find_and_undo (K true)));
wenzelm@29348
    82
wenzelm@29348
    83
fun undo n = edit_history n (fn st => fn hist =>
wenzelm@29348
    84
  find_and_undo (if Toplevel.is_proof st then K true else OuterKeyword.is_theory) hist);
wenzelm@29348
    85
wenzelm@29348
    86
fun kill () = edit_history 1 (fn st => fn hist =>
wenzelm@29348
    87
  find_and_undo
wenzelm@29348
    88
    (if Toplevel.is_proof st then OuterKeyword.is_theory else OuterKeyword.is_theory_begin) hist);
wenzelm@29348
    89
wenzelm@29348
    90
fun kill_proof () = edit_history 1 (fn st => fn hist =>
wenzelm@29348
    91
  if Toplevel.is_proof st then find_and_undo OuterKeyword.is_theory hist
wenzelm@29348
    92
  else raise Toplevel.UNDEF);
wenzelm@29348
    93
wenzelm@29348
    94
end;
wenzelm@29348
    95
wenzelm@29348
    96
wenzelm@29348
    97
(* interactive state transformations *)
wenzelm@29348
    98
wenzelm@29348
    99
fun op >> tr =
wenzelm@29348
   100
  (case Toplevel.transition true tr (state ()) of
wenzelm@29348
   101
    NONE => false
wenzelm@29348
   102
  | SOME (_, SOME err) => (set_exn (SOME err); Toplevel.error_msg tr err; true)
wenzelm@29348
   103
  | SOME (st', NONE) =>
wenzelm@29348
   104
      let
wenzelm@29348
   105
        val name = Toplevel.name_of tr;
wenzelm@29348
   106
        val _ = if OuterKeyword.is_theory_begin name then init () else ();
wenzelm@29348
   107
        val _ =
wenzelm@29348
   108
          if OuterKeyword.is_regular name
wenzelm@29348
   109
          then edit_history 1 (fn st => fn hist => (st', (st, tr) :: hist)) else ();
wenzelm@29348
   110
      in true end);
wenzelm@29348
   111
wenzelm@29348
   112
fun op >>> [] = ()
wenzelm@29348
   113
  | op >>> (tr :: trs) = if op >> tr then op >>> trs else ();
wenzelm@29348
   114
wenzelm@29348
   115
wenzelm@29348
   116
(* toplevel loop *)
wenzelm@29348
   117
wenzelm@29348
   118
val crashes = ref ([]: exn list);
wenzelm@29348
   119
wenzelm@29348
   120
local
wenzelm@29348
   121
wenzelm@29348
   122
fun raw_loop secure src =
wenzelm@29348
   123
  let
wenzelm@29348
   124
    fun check_secure () =
wenzelm@29348
   125
      (if secure then warning "Secure loop -- cannot exit to ML" else (); secure);
wenzelm@29348
   126
  in
wenzelm@29348
   127
    (case Source.get_single (Source.set_prompt Source.default_prompt src) of
wenzelm@29348
   128
      NONE => if secure then quit () else ()
wenzelm@29348
   129
    | SOME (tr, src') => if op >> tr orelse check_secure () then raw_loop secure src' else ())
wenzelm@29370
   130
    handle exn =>
wenzelm@31478
   131
      (Output.error_msg (ML_Compiler.exn_message exn)
wenzelm@29370
   132
        handle crash =>
wenzelm@29370
   133
          (CRITICAL (fn () => change crashes (cons crash));
wenzelm@29370
   134
            warning "Recovering from Isar toplevel crash -- see also Isar.crashes");
wenzelm@29370
   135
          raw_loop secure src)
wenzelm@29348
   136
  end;
wenzelm@29348
   137
wenzelm@29348
   138
in
wenzelm@29348
   139
wenzelm@29348
   140
fun toplevel_loop {init = do_init, welcome, sync, secure} =
wenzelm@29348
   141
 (Context.set_thread_data NONE;
wenzelm@32486
   142
  if do_init then init () else ();
wenzelm@29348
   143
  if welcome then writeln (Session.welcome ()) else ();
wenzelm@29348
   144
  uninterruptible (fn _ => fn () => raw_loop secure (OuterSyntax.isar sync)) ());
wenzelm@29348
   145
wenzelm@29348
   146
end;
wenzelm@29348
   147
wenzelm@29348
   148
fun loop () =
wenzelm@29348
   149
  toplevel_loop {init = false, welcome = false, sync = false, secure = Secure.is_secure ()};
wenzelm@29348
   150
wenzelm@29348
   151
fun main () =
wenzelm@29348
   152
  toplevel_loop {init = true, welcome = true, sync = false, secure = Secure.is_secure ()};
wenzelm@29348
   153
wenzelm@29348
   154
wenzelm@29348
   155
wenzelm@30173
   156
(** command syntax **)
wenzelm@28300
   157
wenzelm@28300
   158
local
wenzelm@28300
   159
wenzelm@30173
   160
structure P = OuterParse and K = OuterKeyword;
wenzelm@28300
   161
val op >> = Scan.>>;
wenzelm@28300
   162
wenzelm@28300
   163
in
wenzelm@28300
   164
wenzelm@30173
   165
(* global history *)
wenzelm@30173
   166
wenzelm@30173
   167
val _ =
wenzelm@30173
   168
  OuterSyntax.improper_command "init_toplevel" "init toplevel point-of-interest" K.control
wenzelm@30173
   169
    (Scan.succeed (Toplevel.no_timing o Toplevel.imperative init));
wenzelm@30173
   170
wenzelm@30173
   171
val _ =
wenzelm@30173
   172
  OuterSyntax.improper_command "linear_undo" "undo commands" K.control
wenzelm@30173
   173
    (Scan.optional P.nat 1 >>
wenzelm@30173
   174
      (fn n => Toplevel.no_timing o Toplevel.imperative (fn () => linear_undo n)));
wenzelm@30173
   175
wenzelm@30173
   176
val _ =
wenzelm@30173
   177
  OuterSyntax.improper_command "undo" "undo commands (skipping closed proofs)" K.control
wenzelm@30173
   178
    (Scan.optional P.nat 1 >>
wenzelm@30173
   179
      (fn n => Toplevel.no_timing o Toplevel.imperative (fn () => undo n)));
wenzelm@30173
   180
wenzelm@30173
   181
val _ =
wenzelm@30173
   182
  OuterSyntax.improper_command "undos_proof" "undo commands (skipping closed proofs)" K.control
wenzelm@30173
   183
    (Scan.optional P.nat 1 >> (fn n => Toplevel.no_timing o
wenzelm@30173
   184
      Toplevel.keep (fn state =>
wenzelm@30173
   185
        if Toplevel.is_proof state then (undo n; print ()) else raise Toplevel.UNDEF)));
wenzelm@30173
   186
wenzelm@30173
   187
val _ =
wenzelm@30173
   188
  OuterSyntax.improper_command "cannot_undo" "partial undo -- Proof General legacy" K.control
wenzelm@30173
   189
    (P.name >>
wenzelm@30173
   190
      (fn "end" => Toplevel.no_timing o Toplevel.imperative (fn () => undo 1)
wenzelm@30173
   191
        | txt => Toplevel.imperative (fn () => error ("Cannot undo " ^ quote txt))));
wenzelm@30173
   192
wenzelm@30173
   193
val _ =
wenzelm@30173
   194
  OuterSyntax.improper_command "kill" "kill partial proof or theory development" K.control
wenzelm@30173
   195
    (Scan.succeed (Toplevel.no_timing o Toplevel.imperative kill));
wenzelm@30173
   196
wenzelm@26605
   197
end;
wenzelm@26605
   198
wenzelm@28300
   199
end;