author  wenzelm 
Wed, 08 Aug 2012 12:33:40 +0200  
changeset 48731  a45ba78abcc1 
parent 48698  2585042b1a30 
child 50917  9459f59cff09 
permissions  rwrr 
30175  1 
(* Title: Pure/System/isar.ML 
26605
24e60e823d22
The global Isabelle/Isar state and main readevalprint loop.
wenzelm
parents:
diff
changeset

2 
Author: Makarius 
24e60e823d22
The global Isabelle/Isar state and main readevalprint 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 readevalprint loop. 
26605
24e60e823d22
The global Isabelle/Isar state and main readevalprint loop.
wenzelm
parents:
diff
changeset

5 
*) 
24e60e823d22
The global Isabelle/Isar state and main readevalprint loop.
wenzelm
parents:
diff
changeset

6 

24e60e823d22
The global Isabelle/Isar state and main readevalprint loop.
wenzelm
parents:
diff
changeset

7 
signature ISAR = 
24e60e823d22
The global Isabelle/Isar state and main readevalprint 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 readevalprint 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 readevalprint loop.
wenzelm
parents:
diff
changeset

14 
val >> : Toplevel.transition > bool 
24e60e823d22
The global Isabelle/Isar state and main readevalprint 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 readevalprint 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 readevalprint loop.
wenzelm
parents:
diff
changeset

25 
end; 
24e60e823d22
The global Isabelle/Isar state and main readevalprint loop.
wenzelm
parents:
diff
changeset

26 

24e60e823d22
The global Isabelle/Isar state and main readevalprint loop.
wenzelm
parents:
diff
changeset

27 
structure Isar: ISAR = 
24e60e823d22
The global Isabelle/Isar state and main readevalprint loop.
wenzelm
parents:
diff
changeset

28 
struct 
24e60e823d22
The global Isabelle/Isar state and main readevalprint 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  SINGLETHREADED! **) 
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 multiexceptions etc.;
wenzelm
parents:
38799
diff
changeset

97 
 SOME (_, SOME exn_info) => 
ec7045139e70
Toplevel.run_command: more careful treatment of interrupts stemming from nested multiexceptions 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 multiexceptions 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  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  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  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  128 
handle exn => 
31478  129 
(Output.error_msg (ML_Compiler.exn_message exn) 
29370  130 
handle crash => 
43684  131 
(Synchronized.change crashes (cons crash); 
29370  132 
warning "Recovering from Isar toplevel crash  see also Isar.crashes"); 
38272  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 readevalprint loop.
wenzelm
parents:
diff
changeset

154 
end; 