src/Pure/System/isar.ML
author wenzelm
Wed, 08 Aug 2012 12:33:40 +0200
changeset 48731 a45ba78abcc1
parent 48698 2585042b1a30
child 50917 9459f59cff09
permissions -rw-r--r--
more casual exit back to ML toplevel, to accomodate commit in SML/NJ which continues at the saved point;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
30175
62ba490670e8 fixed headers;
wenzelm
parents: 30173
diff changeset
     1
(*  Title:      Pure/System/isar.ML
26605
24e60e823d22 The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
24e60e823d22 The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff changeset
     3
37306
2bde06a2a706 discontinued obsolete Isar.context() -- long superseded by @{context};
wenzelm
parents: 37239
diff changeset
     4
Global state of the raw Isar read-eval-print loop.
26605
24e60e823d22 The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff changeset
     5
*)
24e60e823d22 The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff changeset
     6
24e60e823d22 The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff changeset
     7
signature ISAR =
24e60e823d22 The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff changeset
     8
sig
29348
28b0652aabd8 simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents: 29314
diff changeset
     9
  val init: unit -> unit
28b0652aabd8 simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents: 29314
diff changeset
    10
  val exn: unit -> (exn * string) option
26605
24e60e823d22 The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff changeset
    11
  val state: unit -> Toplevel.state
33289
d0c2ef490613 Isar.goal: Proof.simple_goal, not raw version;
wenzelm
parents: 33223
diff changeset
    12
  val goal: unit -> {context: Proof.context, facts: thm list, goal: thm}
27533
85bbd045ac3e added print;
wenzelm
parents: 27530
diff changeset
    13
  val print: unit -> unit
26605
24e60e823d22 The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff changeset
    14
  val >> : Toplevel.transition -> bool
24e60e823d22 The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff changeset
    15
  val >>> : Toplevel.transition list -> unit
27529
6a5ccbb1bca0 added Isar.linear_undo;
wenzelm
parents: 27528
diff changeset
    16
  val linear_undo: int -> unit
27524
cd95da386e9a provide old-style undo operation (still unused);
wenzelm
parents: 27518
diff changeset
    17
  val undo: int -> unit
27530
df14c9cbd21d export init_point;
wenzelm
parents: 27529
diff changeset
    18
  val kill: unit -> unit
df14c9cbd21d export init_point;
wenzelm
parents: 27529
diff changeset
    19
  val kill_proof: unit -> unit
43684
85388f5570c4 prefer Synchronized.var;
wenzelm
parents: 39234
diff changeset
    20
  val crashes: exn list Synchronized.var
38253
3d4e521014f7 Isabelle_Process: separate input fifo for commands (still using the old tty protocol);
wenzelm
parents: 38138
diff changeset
    21
  val toplevel_loop: TextIO.instream ->
3d4e521014f7 Isabelle_Process: separate input fifo for commands (still using the old tty protocol);
wenzelm
parents: 38138
diff changeset
    22
    {init: bool, welcome: bool, sync: bool, secure: bool} -> unit
26605
24e60e823d22 The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff changeset
    23
  val loop: unit -> unit
26606
379596d12f25 replaced Isar loop variants by generic toplevel_loop;
wenzelm
parents: 26605
diff changeset
    24
  val main: unit -> unit
26605
24e60e823d22 The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff changeset
    25
end;
24e60e823d22 The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff changeset
    26
24e60e823d22 The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff changeset
    27
structure Isar: ISAR =
24e60e823d22 The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff changeset
    28
struct
24e60e823d22 The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff changeset
    29
27432
c5ec309c6de8 replaced datatype kind by OuterKeyword.category;
wenzelm
parents: 27428
diff changeset
    30
29348
28b0652aabd8 simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents: 29314
diff changeset
    31
(** TTY model -- SINGLE-THREADED! **)
28b0652aabd8 simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents: 29314
diff changeset
    32
28b0652aabd8 simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents: 29314
diff changeset
    33
(* the global state *)
28b0652aabd8 simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents: 29314
diff changeset
    34
28b0652aabd8 simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents: 29314
diff changeset
    35
type history = (Toplevel.state * Toplevel.transition) list;
28b0652aabd8 simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents: 29314
diff changeset
    36
  (*previous state, state transition -- regular commands only*)
28b0652aabd8 simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents: 29314
diff changeset
    37
28b0652aabd8 simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents: 29314
diff changeset
    38
local
32738
15bb09ca0378 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32486
diff changeset
    39
  val global_history = Unsynchronized.ref ([]: history);
15bb09ca0378 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32486
diff changeset
    40
  val global_state = Unsynchronized.ref Toplevel.toplevel;
15bb09ca0378 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32486
diff changeset
    41
  val global_exn = Unsynchronized.ref (NONE: (exn * string) option);
29348
28b0652aabd8 simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents: 29314
diff changeset
    42
in
28b0652aabd8 simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents: 29314
diff changeset
    43
28b0652aabd8 simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents: 29314
diff changeset
    44
fun edit_history count f = NAMED_CRITICAL "Isar" (fn () =>
28b0652aabd8 simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents: 29314
diff changeset
    45
  let
28b0652aabd8 simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents: 29314
diff changeset
    46
    fun edit 0 (st, hist) = (global_history := hist; global_state := st; global_exn := NONE)
28b0652aabd8 simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents: 29314
diff changeset
    47
      | edit n (st, hist) = edit (n - 1) (f st hist);
28b0652aabd8 simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents: 29314
diff changeset
    48
  in edit count (! global_state, ! global_history) end);
28b0652aabd8 simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents: 29314
diff changeset
    49
33223
d27956b4d3b4 non-critical atomic accesses;
wenzelm
parents: 32786
diff changeset
    50
fun state () = ! global_state;
29348
28b0652aabd8 simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents: 29314
diff changeset
    51
33223
d27956b4d3b4 non-critical atomic accesses;
wenzelm
parents: 32786
diff changeset
    52
fun exn () = ! global_exn;
d27956b4d3b4 non-critical atomic accesses;
wenzelm
parents: 32786
diff changeset
    53
fun set_exn exn =  global_exn := exn;
29348
28b0652aabd8 simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents: 29314
diff changeset
    54
28b0652aabd8 simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents: 29314
diff changeset
    55
end;
28b0652aabd8 simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents: 29314
diff changeset
    56
28b0652aabd8 simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents: 29314
diff changeset
    57
28b0652aabd8 simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents: 29314
diff changeset
    58
fun init () = edit_history 1 (K (K (Toplevel.toplevel, [])));
28b0652aabd8 simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents: 29314
diff changeset
    59
33289
d0c2ef490613 Isar.goal: Proof.simple_goal, not raw version;
wenzelm
parents: 33223
diff changeset
    60
fun goal () = Proof.goal (Toplevel.proof_of (state ()))
29348
28b0652aabd8 simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents: 29314
diff changeset
    61
  handle Toplevel.UNDEF => error "No goal present";
28b0652aabd8 simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents: 29314
diff changeset
    62
28b0652aabd8 simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents: 29314
diff changeset
    63
fun print () = Toplevel.print_state false (state ());
28b0652aabd8 simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents: 29314
diff changeset
    64
28b0652aabd8 simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents: 29314
diff changeset
    65
28b0652aabd8 simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents: 29314
diff changeset
    66
(* history navigation *)
28b0652aabd8 simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents: 29314
diff changeset
    67
28b0652aabd8 simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents: 29314
diff changeset
    68
local
28b0652aabd8 simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents: 29314
diff changeset
    69
28b0652aabd8 simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents: 29314
diff changeset
    70
fun find_and_undo _ [] = error "Undo history exhausted"
28b0652aabd8 simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents: 29314
diff changeset
    71
  | find_and_undo which ((prev, tr) :: hist) =
38138
dc65ed8bbb43 find_and_undo: no need to kill_thy again -- Thy_Info.toplevel_begin_theory does that initially (cf. 3ceccd415145);
wenzelm
parents: 37306
diff changeset
    72
      if which (Toplevel.name_of tr) then (prev, hist) else find_and_undo which hist;
29348
28b0652aabd8 simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents: 29314
diff changeset
    73
28b0652aabd8 simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents: 29314
diff changeset
    74
in
28b0652aabd8 simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents: 29314
diff changeset
    75
28b0652aabd8 simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents: 29314
diff changeset
    76
fun linear_undo n = edit_history n (K (find_and_undo (K true)));
28b0652aabd8 simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents: 29314
diff changeset
    77
28b0652aabd8 simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents: 29314
diff changeset
    78
fun undo n = edit_history n (fn st => fn hist =>
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 33289
diff changeset
    79
  find_and_undo (if Toplevel.is_proof st then K true else Keyword.is_theory) hist);
29348
28b0652aabd8 simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents: 29314
diff changeset
    80
28b0652aabd8 simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents: 29314
diff changeset
    81
fun kill () = edit_history 1 (fn st => fn hist =>
28b0652aabd8 simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents: 29314
diff changeset
    82
  find_and_undo
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 33289
diff changeset
    83
    (if Toplevel.is_proof st then Keyword.is_theory else Keyword.is_theory_begin) hist);
29348
28b0652aabd8 simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents: 29314
diff changeset
    84
28b0652aabd8 simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents: 29314
diff changeset
    85
fun kill_proof () = edit_history 1 (fn st => fn hist =>
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 33289
diff changeset
    86
  if Toplevel.is_proof st then find_and_undo Keyword.is_theory hist
29348
28b0652aabd8 simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents: 29314
diff changeset
    87
  else raise Toplevel.UNDEF);
28b0652aabd8 simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents: 29314
diff changeset
    88
28b0652aabd8 simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents: 29314
diff changeset
    89
end;
28b0652aabd8 simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents: 29314
diff changeset
    90
28b0652aabd8 simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents: 29314
diff changeset
    91
28b0652aabd8 simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents: 29314
diff changeset
    92
(* interactive state transformations *)
28b0652aabd8 simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents: 29314
diff changeset
    93
28b0652aabd8 simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents: 29314
diff changeset
    94
fun op >> tr =
28b0652aabd8 simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents: 29314
diff changeset
    95
  (case Toplevel.transition true tr (state ()) of
28b0652aabd8 simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents: 29314
diff changeset
    96
    NONE => false
38876
ec7045139e70 Toplevel.run_command: more careful treatment of interrupts stemming from nested multi-exceptions etc.;
wenzelm
parents: 38799
diff changeset
    97
  | SOME (_, SOME exn_info) =>
ec7045139e70 Toplevel.run_command: more careful treatment of interrupts stemming from nested multi-exceptions etc.;
wenzelm
parents: 38799
diff changeset
    98
     (set_exn (SOME exn_info);
44270
3eaad39e520c more careful treatment of exception serial numbers, with propagation to message channel;
wenzelm
parents: 43684
diff changeset
    99
      Toplevel.error_msg tr (serial (), ML_Compiler.exn_message (Runtime.EXCURSION_FAIL exn_info));
38876
ec7045139e70 Toplevel.run_command: more careful treatment of interrupts stemming from nested multi-exceptions etc.;
wenzelm
parents: 38799
diff changeset
   100
      true)
29348
28b0652aabd8 simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents: 29314
diff changeset
   101
  | SOME (st', NONE) =>
28b0652aabd8 simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents: 29314
diff changeset
   102
      let
28b0652aabd8 simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents: 29314
diff changeset
   103
        val name = Toplevel.name_of tr;
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 33289
diff changeset
   104
        val _ = if Keyword.is_theory_begin name then init () else ();
29348
28b0652aabd8 simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents: 29314
diff changeset
   105
        val _ =
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 33289
diff changeset
   106
          if Keyword.is_regular name
29348
28b0652aabd8 simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents: 29314
diff changeset
   107
          then edit_history 1 (fn st => fn hist => (st', (st, tr) :: hist)) else ();
28b0652aabd8 simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents: 29314
diff changeset
   108
      in true end);
28b0652aabd8 simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents: 29314
diff changeset
   109
28b0652aabd8 simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents: 29314
diff changeset
   110
fun op >>> [] = ()
28b0652aabd8 simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents: 29314
diff changeset
   111
  | op >>> (tr :: trs) = if op >> tr then op >>> trs else ();
28b0652aabd8 simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents: 29314
diff changeset
   112
28b0652aabd8 simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents: 29314
diff changeset
   113
39234
d76a2fd129b5 main command loops are supposed to be uninterruptible -- no special treatment here;
wenzelm
parents: 38876
diff changeset
   114
(* toplevel loop -- uninterruptible *)
29348
28b0652aabd8 simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents: 29314
diff changeset
   115
43684
85388f5570c4 prefer Synchronized.var;
wenzelm
parents: 39234
diff changeset
   116
val crashes = Synchronized.var "Isar.crashes" ([]: exn list);
29348
28b0652aabd8 simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents: 29314
diff changeset
   117
28b0652aabd8 simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents: 29314
diff changeset
   118
local
28b0652aabd8 simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents: 29314
diff changeset
   119
28b0652aabd8 simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents: 29314
diff changeset
   120
fun raw_loop secure src =
28b0652aabd8 simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents: 29314
diff changeset
   121
  let
28b0652aabd8 simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents: 29314
diff changeset
   122
    fun check_secure () =
28b0652aabd8 simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents: 29314
diff changeset
   123
      (if secure then warning "Secure loop -- cannot exit to ML" else (); secure);
28b0652aabd8 simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents: 29314
diff changeset
   124
  in
28b0652aabd8 simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents: 29314
diff changeset
   125
    (case Source.get_single (Source.set_prompt Source.default_prompt src) of
28b0652aabd8 simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents: 29314
diff changeset
   126
      NONE => if secure then quit () else ()
28b0652aabd8 simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents: 29314
diff changeset
   127
    | SOME (tr, src') => if op >> tr orelse check_secure () then raw_loop secure src' else ())
29370
wenzelm
parents: 29348
diff changeset
   128
    handle exn =>
31478
5e412e4c6546 ML_Compiler.exn_message;
wenzelm
parents: 31443
diff changeset
   129
      (Output.error_msg (ML_Compiler.exn_message exn)
29370
wenzelm
parents: 29348
diff changeset
   130
        handle crash =>
43684
85388f5570c4 prefer Synchronized.var;
wenzelm
parents: 39234
diff changeset
   131
          (Synchronized.change crashes (cons crash);
29370
wenzelm
parents: 29348
diff changeset
   132
            warning "Recovering from Isar toplevel crash -- see also Isar.crashes");
38272
wenzelm
parents: 38253
diff changeset
   133
        raw_loop secure src)
29348
28b0652aabd8 simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents: 29314
diff changeset
   134
  end;
28b0652aabd8 simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents: 29314
diff changeset
   135
28b0652aabd8 simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents: 29314
diff changeset
   136
in
28b0652aabd8 simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents: 29314
diff changeset
   137
38253
3d4e521014f7 Isabelle_Process: separate input fifo for commands (still using the old tty protocol);
wenzelm
parents: 38138
diff changeset
   138
fun toplevel_loop in_stream {init = do_init, welcome, sync, secure} =
29348
28b0652aabd8 simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents: 29314
diff changeset
   139
 (Context.set_thread_data NONE;
48698
2585042b1a30 pass Isabelle/Scala system options into ML process of Isar tty or build jobs;
wenzelm
parents: 48646
diff changeset
   140
  if do_init then (Options.load_default (); init ()) else ();
29348
28b0652aabd8 simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents: 29314
diff changeset
   141
  if welcome then writeln (Session.welcome ()) else ();
38253
3d4e521014f7 Isabelle_Process: separate input fifo for commands (still using the old tty protocol);
wenzelm
parents: 38138
diff changeset
   142
  uninterruptible (fn _ => fn () => raw_loop secure (Outer_Syntax.isar in_stream sync)) ());
29348
28b0652aabd8 simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents: 29314
diff changeset
   143
28b0652aabd8 simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents: 29314
diff changeset
   144
end;
28b0652aabd8 simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents: 29314
diff changeset
   145
28b0652aabd8 simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents: 29314
diff changeset
   146
fun loop () =
38253
3d4e521014f7 Isabelle_Process: separate input fifo for commands (still using the old tty protocol);
wenzelm
parents: 38138
diff changeset
   147
  toplevel_loop TextIO.stdIn
3d4e521014f7 Isabelle_Process: separate input fifo for commands (still using the old tty protocol);
wenzelm
parents: 38138
diff changeset
   148
    {init = false, welcome = false, sync = false, secure = Secure.is_secure ()};
29348
28b0652aabd8 simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents: 29314
diff changeset
   149
28b0652aabd8 simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents: 29314
diff changeset
   150
fun main () =
38253
3d4e521014f7 Isabelle_Process: separate input fifo for commands (still using the old tty protocol);
wenzelm
parents: 38138
diff changeset
   151
  toplevel_loop TextIO.stdIn
3d4e521014f7 Isabelle_Process: separate input fifo for commands (still using the old tty protocol);
wenzelm
parents: 38138
diff changeset
   152
    {init = true, welcome = true, sync = false, secure = Secure.is_secure ()};
29348
28b0652aabd8 simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents: 29314
diff changeset
   153
26605
24e60e823d22 The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff changeset
   154
end;