author | wenzelm |
Wed, 11 Dec 2013 18:02:22 +0100 | |
changeset 54717 | 42c209a6c225 |
parent 54387 | 890e983cb07b |
child 55387 | 51f0876f61df |
permissions | -rw-r--r-- |
30175 | 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 | 12 |
val goal: unit -> {context: Proof.context, facts: thm list, goal: thm} |
27533 | 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 | 16 |
val linear_undo: int -> unit |
27524 | 17 |
val undo: int -> unit |
27530 | 18 |
val kill: unit -> unit |
19 |
val kill_proof: unit -> unit |
|
43684 | 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 | 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 | 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); |
|
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 | 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 | 52 |
fun exn () = ! global_exn; |
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 | 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 | 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 | 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 | 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); |
50917 | 99 |
Toplevel.setmp_thread_position tr |
54387 | 100 |
ML_Compiler.exn_error_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
|
101 |
true) |
29348
28b0652aabd8
simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents:
29314
diff
changeset
|
102 |
| SOME (st', NONE) => |
28b0652aabd8
simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents:
29314
diff
changeset
|
103 |
let |
28b0652aabd8
simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents:
29314
diff
changeset
|
104 |
val name = Toplevel.name_of tr; |
36950 | 105 |
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
|
106 |
val _ = |
36950 | 107 |
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
|
108 |
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
|
109 |
in true end); |
28b0652aabd8
simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents:
29314
diff
changeset
|
110 |
|
28b0652aabd8
simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents:
29314
diff
changeset
|
111 |
fun op >>> [] = () |
28b0652aabd8
simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents:
29314
diff
changeset
|
112 |
| 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
|
113 |
|
28b0652aabd8
simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents:
29314
diff
changeset
|
114 |
|
39234
d76a2fd129b5
main command loops are supposed to be uninterruptible -- no special treatment here;
wenzelm
parents:
38876
diff
changeset
|
115 |
(* toplevel loop -- uninterruptible *) |
29348
28b0652aabd8
simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents:
29314
diff
changeset
|
116 |
|
43684 | 117 |
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
|
118 |
|
28b0652aabd8
simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents:
29314
diff
changeset
|
119 |
local |
28b0652aabd8
simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents:
29314
diff
changeset
|
120 |
|
51662
3391a493f39a
just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
wenzelm
parents:
50917
diff
changeset
|
121 |
fun protocol_message props output = |
3391a493f39a
just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
wenzelm
parents:
50917
diff
changeset
|
122 |
(case props of |
3391a493f39a
just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
wenzelm
parents:
50917
diff
changeset
|
123 |
function :: args => |
3391a493f39a
just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
wenzelm
parents:
50917
diff
changeset
|
124 |
if function = Markup.command_timing then |
3391a493f39a
just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
wenzelm
parents:
50917
diff
changeset
|
125 |
let |
3391a493f39a
just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
wenzelm
parents:
50917
diff
changeset
|
126 |
val name = the_default "" (Properties.get args Markup.nameN); |
3391a493f39a
just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
wenzelm
parents:
50917
diff
changeset
|
127 |
val pos = Position.of_properties args; |
3391a493f39a
just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
wenzelm
parents:
50917
diff
changeset
|
128 |
val timing = Markup.parse_timing_properties args; |
3391a493f39a
just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
wenzelm
parents:
50917
diff
changeset
|
129 |
in |
3391a493f39a
just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
wenzelm
parents:
50917
diff
changeset
|
130 |
if Timing.is_relevant timing andalso (! Toplevel.profiling > 0 orelse ! Toplevel.timing) |
3391a493f39a
just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
wenzelm
parents:
50917
diff
changeset
|
131 |
andalso name <> "" andalso not (Keyword.is_control name) |
3391a493f39a
just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
wenzelm
parents:
50917
diff
changeset
|
132 |
then tracing ("command " ^ quote name ^ Position.here pos ^ ": " ^ Timing.message timing) |
3391a493f39a
just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
wenzelm
parents:
50917
diff
changeset
|
133 |
else () |
3391a493f39a
just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
wenzelm
parents:
50917
diff
changeset
|
134 |
end |
3391a493f39a
just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
wenzelm
parents:
50917
diff
changeset
|
135 |
else raise Output.Protocol_Message props |
3391a493f39a
just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
wenzelm
parents:
50917
diff
changeset
|
136 |
| [] => raise Output.Protocol_Message props); |
3391a493f39a
just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
wenzelm
parents:
50917
diff
changeset
|
137 |
|
29348
28b0652aabd8
simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents:
29314
diff
changeset
|
138 |
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
|
139 |
let |
28b0652aabd8
simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents:
29314
diff
changeset
|
140 |
fun check_secure () = |
28b0652aabd8
simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents:
29314
diff
changeset
|
141 |
(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
|
142 |
in |
28b0652aabd8
simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents:
29314
diff
changeset
|
143 |
(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
|
144 |
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
|
145 |
| SOME (tr, src') => if op >> tr orelse check_secure () then raw_loop secure src' else ()) |
29370 | 146 |
handle exn => |
54387 | 147 |
(ML_Compiler.exn_error_message exn |
29370 | 148 |
handle crash => |
43684 | 149 |
(Synchronized.change crashes (cons crash); |
29370 | 150 |
warning "Recovering from Isar toplevel crash -- see also Isar.crashes"); |
38272 | 151 |
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
|
152 |
end; |
28b0652aabd8
simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents:
29314
diff
changeset
|
153 |
|
28b0652aabd8
simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents:
29314
diff
changeset
|
154 |
in |
28b0652aabd8
simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents:
29314
diff
changeset
|
155 |
|
38253
3d4e521014f7
Isabelle_Process: separate input fifo for commands (still using the old tty protocol);
wenzelm
parents:
38138
diff
changeset
|
156 |
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
|
157 |
(Context.set_thread_data NONE; |
54717 | 158 |
Multithreading.max_threads_update (Options.default_int "threads"); |
51948
cb5dbc9a06f9
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
parents:
51662
diff
changeset
|
159 |
if do_init then init () else (); |
52852 | 160 |
Output.Internal.protocol_message_fn := protocol_message; |
29348
28b0652aabd8
simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents:
29314
diff
changeset
|
161 |
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
|
162 |
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
|
163 |
|
28b0652aabd8
simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents:
29314
diff
changeset
|
164 |
end; |
28b0652aabd8
simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents:
29314
diff
changeset
|
165 |
|
28b0652aabd8
simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents:
29314
diff
changeset
|
166 |
fun loop () = |
38253
3d4e521014f7
Isabelle_Process: separate input fifo for commands (still using the old tty protocol);
wenzelm
parents:
38138
diff
changeset
|
167 |
toplevel_loop TextIO.stdIn |
3d4e521014f7
Isabelle_Process: separate input fifo for commands (still using the old tty protocol);
wenzelm
parents:
38138
diff
changeset
|
168 |
{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
|
169 |
|
28b0652aabd8
simplified tty model -- back to plain list history, which is independent of editor model;
wenzelm
parents:
29314
diff
changeset
|
170 |
fun main () = |
38253
3d4e521014f7
Isabelle_Process: separate input fifo for commands (still using the old tty protocol);
wenzelm
parents:
38138
diff
changeset
|
171 |
toplevel_loop TextIO.stdIn |
3d4e521014f7
Isabelle_Process: separate input fifo for commands (still using the old tty protocol);
wenzelm
parents:
38138
diff
changeset
|
172 |
{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
|
173 |
|
26605
24e60e823d22
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm
parents:
diff
changeset
|
174 |
end; |