author  wenzelm 
Sat, 11 May 2013 20:10:24 +0200  
changeset 51933  a60c6c90a447 
parent 51606  2843cc095a57 
child 51947  3301612c4893 
permissions  rwrr 
31432
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

1 
(** Pure Isabelle **) 
0  2 

26109
c69c3559355b
more elaborate structure Distribution (filledin by makedist);
wenzelm
parents:
25953
diff
changeset

3 
structure Distribution = (*filledin by makedist*) 
c69c3559355b
more elaborate structure Distribution (filledin by makedist);
wenzelm
parents:
25953
diff
changeset

4 
struct 
32361
141e5151b918
clarified situation about unidentified repository versions  in a distributed setting there is not "the" repository;
wenzelm
parents:
32187
diff
changeset

5 
val version = "unidentified repository version"; 
27642
c0db1220b071
structure Distribution: swapped default for is_official;
wenzelm
parents:
27546
diff
changeset

6 
val is_official = false; 
26109
c69c3559355b
more elaborate structure Distribution (filledin by makedist);
wenzelm
parents:
25953
diff
changeset

7 
end; 
11835  8 

23825
e0372eba47b7
simplified loading of ML files  no static forward references;
wenzelm
parents:
23696
diff
changeset

9 
(*if true then some tools will OMIT some proofs*) 
32738  10 
val quick_and_dirty = Unsynchronized.ref false; 
23825
e0372eba47b7
simplified loading of ML files  no static forward references;
wenzelm
parents:
23696
diff
changeset

11 

12248  12 
print_depth 10; 
0  13 

31432
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

14 

9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

15 
(* library of general tools *) 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

16 

21396  17 
use "General/basics.ML"; 
0  18 
use "library.ML"; 
31432
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

19 
use "General/print_mode.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

20 
use "General/alist.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

21 
use "General/table.ML"; 
43684  22 

23 
use "Concurrent/simple_thread.ML"; 

24 

25 
use "Concurrent/synchronized.ML"; 

26 
if Multithreading.available then () 

27 
else use "Concurrent/synchronized_sequential.ML"; 

28 

43746
a41f618c641d
some support for raw messages, which bypass standard Symbol/YXML decoding;
wenzelm
parents:
43729
diff
changeset

29 
use "General/properties.ML"; 
31432
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

30 
use "General/output.ML"; 
45670  31 
use "PIDE/markup.ML"; 
50201
c26369c9eda6
Isabellespecific implementation of quasiabstract markup elements  back to module arrangement before d83797ef0d2d;
wenzelm
parents:
50163
diff
changeset

32 
fun legacy_feature s = warning (Markup.markup Markup.legacy ("Legacy feature! " ^ s)); 
51606
2843cc095a57
additional timing status for implicitly forked terminal proofs  proper accounting for interactive Timing dockable etc.;
wenzelm
parents:
51551
diff
changeset

33 
use "General/timing.ML"; 
31432
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

34 
use "General/scan.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

35 
use "General/source.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

36 
use "General/symbol.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

37 
use "General/seq.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

38 
use "General/position.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

39 
use "General/symbol_pos.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

40 
use "General/antiquote.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

41 
use "ML/ml_lex.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

42 
use "ML/ml_parse.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

43 
use "General/secure.ML"; 
32015
7101feb5247e
Support for copyavoiding functions on pure values, at the cost of readability.
wenzelm
parents:
31476
diff
changeset

44 
(*^^^^^ end of basic ML bootstrap ^^^^^*) 
31432
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

45 
use "General/integer.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

46 
use "General/stack.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

47 
use "General/queue.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

48 
use "General/heap.ML"; 
32015
7101feb5247e
Support for copyavoiding functions on pure values, at the cost of readability.
wenzelm
parents:
31476
diff
changeset

49 
use "General/same.ML"; 
31432
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

50 
use "General/ord_list.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

51 
use "General/balanced_tree.ML"; 
38448
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38418
diff
changeset

52 
use "General/linear_set.ML"; 
43593  53 
use "General/buffer.ML"; 
43791  54 
use "General/pretty.ML"; 
31432
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

55 
use "General/path.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

56 
use "General/url.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

57 
use "General/file.ML"; 
43547
f3a8476285c6
clarified Binding.pretty/print: no quotes, only markup  Binding.str_of is rendered obsolete;
wenzelm
parents:
42504
diff
changeset

58 
use "General/long_name.ML"; 
f3a8476285c6
clarified Binding.pretty/print: no quotes, only markup  Binding.str_of is rendered obsolete;
wenzelm
parents:
42504
diff
changeset

59 
use "General/binding.ML"; 
50800
c0fb2839d1a9
recovered buffered sockets from 11f622794ad6  requires Poly/ML 5.5.x;
wenzelm
parents:
50757
diff
changeset

60 
use "General/socket_io.ML"; 
22592  61 

35628  62 
use "General/sha1.ML"; 
43948  63 
if ML_System.is_polyml then use "General/sha1_polyml.ML" else (); 
35628  64 

44698  65 
use "PIDE/xml.ML"; 
66 
use "PIDE/yxml.ML"; 

67 

49560  68 
use "General/graph.ML"; 
69 

31432
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

70 

9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

71 
(* concurrency within the ML runtime *) 
28120  72 

50911
ee7fe4230642
more explicit treatment of (optional) exception properties, notably for "serial"  avoid conflict with startPosition = offset;
wenzelm
parents:
50800
diff
changeset

73 
if ML_System.is_polyml 
ee7fe4230642
more explicit treatment of (optional) exception properties, notably for "serial"  avoid conflict with startPosition = offset;
wenzelm
parents:
50800
diff
changeset

74 
then use "ML/exn_properties_polyml.ML" 
ee7fe4230642
more explicit treatment of (optional) exception properties, notably for "serial"  avoid conflict with startPosition = offset;
wenzelm
parents:
50800
diff
changeset

75 
else use "ML/exn_properties_dummy.ML"; 
ee7fe4230642
more explicit treatment of (optional) exception properties, notably for "serial"  avoid conflict with startPosition = offset;
wenzelm
parents:
50800
diff
changeset

76 

50255  77 
if ML_System.name = "polyml5.5.0" 
78 
then use "ML/ml_statistics_polyml5.5.0.ML" 

79 
else use "ML/ml_statistics_dummy.ML"; 

80 

35014
a725ff6ead26
explicit representation of singleassignment variables;
wenzelm
parents:
33538
diff
changeset

81 
use "Concurrent/single_assignment.ML"; 
a725ff6ead26
explicit representation of singleassignment variables;
wenzelm
parents:
33538
diff
changeset

82 
if Multithreading.available then () 
a725ff6ead26
explicit representation of singleassignment variables;
wenzelm
parents:
33538
diff
changeset

83 
else use "Concurrent/single_assignment_sequential.ML"; 
a725ff6ead26
explicit representation of singleassignment variables;
wenzelm
parents:
33538
diff
changeset

84 

47980
c81801f881b3
simplified Poly/ML setup  5.3.0 is now the common baseline;
wenzelm
parents:
47979
diff
changeset

85 
if ML_System.is_polyml then use "Concurrent/time_limit.ML" else (); 
41710  86 

40748
591b6778d076
removed bash from ML system bootstrap, and past the Secure ML barrier;
wenzelm
parents:
40743
diff
changeset

87 
if Multithreading.available 
591b6778d076
removed bash from ML system bootstrap, and past the Secure ML barrier;
wenzelm
parents:
40743
diff
changeset

88 
then use "Concurrent/bash.ML" 
591b6778d076
removed bash from ML system bootstrap, and past the Secure ML barrier;
wenzelm
parents:
40743
diff
changeset

89 
else use "Concurrent/bash_sequential.ML"; 
591b6778d076
removed bash from ML system bootstrap, and past the Secure ML barrier;
wenzelm
parents:
40743
diff
changeset

90 

44247  91 
use "Concurrent/par_exn.ML"; 
31432
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

92 
use "Concurrent/task_queue.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

93 
use "Concurrent/future.ML"; 
32840  94 

32815
1a5e364584ae
separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents:
32738
diff
changeset

95 
use "Concurrent/lazy.ML"; 
1a5e364584ae
separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents:
32738
diff
changeset

96 
if Multithreading.available then () 
1a5e364584ae
separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents:
32738
diff
changeset

97 
else use "Concurrent/lazy_sequential.ML"; 
32840  98 

31432
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

99 
use "Concurrent/par_list.ML"; 
32815
1a5e364584ae
separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents:
32738
diff
changeset

100 
if Multithreading.available then () 
32816
5db89f8d44f3
more official status of sequential implementations;
wenzelm
parents:
32815
diff
changeset

101 
else use "Concurrent/par_list_sequential.ML"; 
31432
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

102 

44247  103 
use "Concurrent/mailbox.ML"; 
32840  104 
use "Concurrent/cache.ML"; 
105 

50500
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset

106 
use "PIDE/active.ML"; 
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset

107 

31432
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

108 

9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

109 
(* fundamental structures *) 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

110 

20075  111 
use "name.ML"; 
0  112 
use "term.ML"; 
28404  113 
use "context.ML"; 
47813  114 
use "context_position.ML"; 
39508
dfacdb01e1ec
simplified some internal flags using Config.T instead of fullblown Proof_Data;
wenzelm
parents:
39290
diff
changeset

115 
use "config.ML"; 
48456
d8ff14f44a40
added ML version of standalone options, with XML.encode/decode operations (unidirectional from Scala to ML);
wenzelm
parents:
48418
diff
changeset

116 
use "System/options.ML"; 
19  117 

31432
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

118 

9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

119 
(* inner syntax *) 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

120 

42264  121 
use "Syntax/term_position.ML"; 
122 
use "Syntax/lexicon.ML"; 

22679  123 
use "Syntax/ast.ML"; 
42288
2074b31650e6
discontinued special treatment of structure Syntax_Ext (formerly Syn_Ext);
wenzelm
parents:
42284
diff
changeset

124 
use "Syntax/syntax_ext.ML"; 
22679  125 
use "Syntax/parser.ML"; 
42284  126 
use "Syntax/syntax_trans.ML"; 
22679  127 
use "Syntax/mixfix.ML"; 
128 
use "Syntax/printer.ML"; 

129 
use "Syntax/syntax.ML"; 

130 

31432
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

131 

9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

132 
(* core of tactical proof system *) 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

133 

42382
dcd983ee2c29
provide structure Syntax early (before structure Type), backpatch check/uncheck later;
wenzelm
parents:
42357
diff
changeset

134 
use "term_ord.ML"; 
dcd983ee2c29
provide structure Syntax early (before structure Type), backpatch check/uncheck later;
wenzelm
parents:
42357
diff
changeset

135 
use "term_subst.ML"; 
43729  136 
use "term_xml.ML"; 
42382
dcd983ee2c29
provide structure Syntax early (before structure Type), backpatch check/uncheck later;
wenzelm
parents:
42357
diff
changeset

137 
use "General/name_space.ML"; 
dcd983ee2c29
provide structure Syntax early (before structure Type), backpatch check/uncheck later;
wenzelm
parents:
42357
diff
changeset

138 
use "sorts.ML"; 
dcd983ee2c29
provide structure Syntax early (before structure Type), backpatch check/uncheck later;
wenzelm
parents:
42357
diff
changeset

139 
use "type.ML"; 
dcd983ee2c29
provide structure Syntax early (before structure Type), backpatch check/uncheck later;
wenzelm
parents:
42357
diff
changeset

140 
use "logic.ML"; 
dcd983ee2c29
provide structure Syntax early (before structure Type), backpatch check/uncheck later;
wenzelm
parents:
42357
diff
changeset

141 
use "Syntax/simple_syntax.ML"; 
30559
e5987a7ac5df
turned structure NetRules into general Item_Net, which is loaded earlier;
wenzelm
parents:
30173
diff
changeset

142 
use "net.ML"; 
e5987a7ac5df
turned structure NetRules into general Item_Net, which is loaded earlier;
wenzelm
parents:
30173
diff
changeset

143 
use "item_net.ML"; 
18934  144 
use "envir.ML"; 
18059  145 
use "consts.ML"; 
24257  146 
use "primitive_defs.ML"; 
27546  147 
use "defs.ML"; 
0  148 
use "sign.ML"; 
43795
ca5896a836ba
recovered some runtime sharing from d6b6c74a8bcf, without the global memory bottleneck;
wenzelm
parents:
43794
diff
changeset

149 
use "term_sharing.ML"; 
0  150 
use "pattern.ML"; 
151 
use "unify.ML"; 

1528  152 
use "theory.ML"; 
24664  153 
use "interpretation.ML"; 
11511  154 
use "proofterm.ML"; 
0  155 
use "thm.ML"; 
22361  156 
use "more_thm.ML"; 
26279  157 
use "facts.ML"; 
39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is globalonly;
wenzelm
parents:
39508
diff
changeset

158 
use "global_theory.ML"; 
3986  159 
use "pure_thy.ML"; 
0  160 
use "drule.ML"; 
22233  161 
use "morphism.ML"; 
19898  162 
use "variable.ML"; 
24833  163 
use "conv.ML"; 
32187  164 
use "goal_display.ML"; 
32169  165 
use "tactical.ML"; 
1582  166 
use "search.ML"; 
21708  167 
use "tactic.ML"; 
41228
e1fce873b814
renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
wenzelm
parents:
40748
diff
changeset

168 
use "raw_simplifier.ML"; 
19417  169 
use "conjunction.ML"; 
20225  170 
use "assumption.ML"; 
32089
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
32015
diff
changeset

171 
use "display.ML"; 
0  172 

31432
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

173 

9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

174 
(* Isar  Intelligible SemiAutomated Reasoning *) 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

175 

49041
9edfd36a0355
more informative error message from failed goal forks (violating oldstyle TTY protocol!);
wenzelm
parents:
48990
diff
changeset

176 
(*ML support*) 
9edfd36a0355
more informative error message from failed goal forks (violating oldstyle TTY protocol!);
wenzelm
parents:
48990
diff
changeset

177 
use "ML/ml_syntax.ML"; 
9edfd36a0355
more informative error message from failed goal forks (violating oldstyle TTY protocol!);
wenzelm
parents:
48990
diff
changeset

178 
use "ML/ml_env.ML"; 
9edfd36a0355
more informative error message from failed goal forks (violating oldstyle TTY protocol!);
wenzelm
parents:
48990
diff
changeset

179 
use "Isar/runtime.ML"; 
9edfd36a0355
more informative error message from failed goal forks (violating oldstyle TTY protocol!);
wenzelm
parents:
48990
diff
changeset

180 
use "ML/ml_compiler.ML"; 
9edfd36a0355
more informative error message from failed goal forks (violating oldstyle TTY protocol!);
wenzelm
parents:
48990
diff
changeset

181 
if ML_System.is_polyml then use "ML/ml_compiler_polyml.ML" else (); 
9edfd36a0355
more informative error message from failed goal forks (violating oldstyle TTY protocol!);
wenzelm
parents:
48990
diff
changeset

182 

51551  183 
use "skip_proof.ML"; 
49041
9edfd36a0355
more informative error message from failed goal forks (violating oldstyle TTY protocol!);
wenzelm
parents:
48990
diff
changeset

184 
use "goal.ML"; 
9edfd36a0355
more informative error message from failed goal forks (violating oldstyle TTY protocol!);
wenzelm
parents:
48990
diff
changeset

185 

31432
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

186 
(*proof context*) 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

187 
use "Isar/object_logic.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

188 
use "Isar/rule_cases.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

189 
use "Isar/auto_bind.ML"; 
42241
dd8029f71e1c
separate module for standard implementation of inner syntax operations;
wenzelm
parents:
42240
diff
changeset

190 
use "type_infer.ML"; 
42240
5a4d30cd47a7
moved Isar/local_syntax.ML to Syntax/local_syntax.ML;
wenzelm
parents:
42012
diff
changeset

191 
use "Syntax/local_syntax.ML"; 
31432
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

192 
use "Isar/proof_context.ML"; 
42405
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
42383
diff
changeset

193 
use "type_infer_context.ML"; 
42243  194 
use "Syntax/syntax_phases.ML"; 
31432
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

195 
use "Isar/local_defs.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

196 

9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

197 
(*proof term operations*) 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

198 
use "Proof/reconstruct.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

199 
use "Proof/proof_syntax.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

200 
use "Proof/proof_rewrite_rules.ML"; 
44062  201 
use "Proof/proof_checker.ML"; 
31432
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

202 

9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

203 
(*outer syntax*) 
36959
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
36955
diff
changeset

204 
use "Isar/token.ML"; 
36949
080e85d46108
renamed structure OuterKeyword to Keyword and OuterParse to Parse, keeping the old names as legacy aliases for some time;
wenzelm
parents:
35949
diff
changeset

205 
use "Isar/keyword.ML"; 
080e85d46108
renamed structure OuterKeyword to Keyword and OuterParse to Parse, keeping the old names as legacy aliases for some time;
wenzelm
parents:
35949
diff
changeset

206 
use "Isar/parse.ML"; 
31432
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

207 
use "Isar/args.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

208 
use "ML/ml_context.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

209 

9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

210 
(*theory sources*) 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

211 
use "Thy/thy_header.ML"; 
51265  212 
use "Thy/thy_syntax.ML"; 
31432
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

213 
use "Thy/html.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

214 
use "Thy/latex.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

215 

9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

216 
(*basic proof engine*) 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

217 
use "Isar/proof_display.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

218 
use "Isar/attrib.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

219 
use "ML/ml_antiquote.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

220 
use "Isar/context_rules.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

221 
use "Isar/method.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

222 
use "Isar/proof.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

223 
use "Isar/element.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

224 

9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

225 
(*derived theory and proof elements*) 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

226 
use "Isar/calculation.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

227 
use "Isar/obtain.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

228 

9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

229 
(*local theories and targets*) 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

230 
use "Isar/local_theory.ML"; 
38341
72dba5bd5f63
moved theorylevel target operation fragements to Generic_Target; adjusted bootstrap order
haftmann
parents:
38307
diff
changeset

231 
use "Isar/locale.ML"; 
38307
0028571ade2d
split off structure Generic_Target into separate file
haftmann
parents:
38150
diff
changeset

232 
use "Isar/generic_target.ML"; 
31432
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

233 
use "Isar/overloading.ML"; 
35669
a91c7ed801b8
added ProofContext.tsig_of  proforma version for local name space only, not logical content;
wenzelm
parents:
35628
diff
changeset

234 
use "axclass.ML"; 
38379
67d71449e85b
more convenient split of class modules: class and class_declaration
haftmann
parents:
38350
diff
changeset

235 
use "Isar/class.ML"; 
38350
480b2de9927c
renamed Theory_Target to the more appropriate Named_Target
haftmann
parents:
38343
diff
changeset

236 
use "Isar/named_target.ML"; 
31432
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

237 
use "Isar/expression.ML"; 
38379
67d71449e85b
more convenient split of class modules: class and class_declaration
haftmann
parents:
38350
diff
changeset

238 
use "Isar/class_declaration.ML"; 
47057  239 
use "Isar/bundle.ML"; 
31432
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

240 

9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

241 
use "simplifier.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

242 

9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

243 
(*executable theory content*) 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

244 
use "Isar/code.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

245 

9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

246 
(*specifications*) 
36952
338c3f8229e4
renamed structure SpecParse to Parse_Spec, keeping the old name as alias for some time;
wenzelm
parents:
36951
diff
changeset

247 
use "Isar/parse_spec.ML"; 
33374
8099185908a4
Rules that characterize functional/relational specifications.
wenzelm
parents:
32840
diff
changeset

248 
use "Isar/spec_rules.ML"; 
31432
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

249 
use "Isar/specification.ML"; 
35626  250 
use "Isar/typedecl.ML"; 
45592  251 
use "ML/ml_thms.ML"; 
31432
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

252 

9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

253 
(*toplevel transactions*) 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

254 
use "Isar/proof_node.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

255 
use "Isar/toplevel.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

256 

38271
36187e8443dd
Isar_Document command input via native Isabelle_Process commands, using YXML and XML_Data representation;
wenzelm
parents:
38266
diff
changeset

257 
(*theory documents*) 
40743  258 
use "System/isabelle_system.ML"; 
31432
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

259 
use "Thy/term_style.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

260 
use "Thy/thy_output.ML"; 
48771
2ea997196d04
clarified Command.range vs. Command.proper_range according to Scala version, which is potentially relevant for command status markup;
wenzelm
parents:
48732
diff
changeset

261 
use "PIDE/command.ML"; 
31432
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

262 
use "Isar/outer_syntax.ML"; 
49561  263 
use "General/graph_display.ML"; 
43712
3c2c912af2ef
moved Outer_Syntax.load_thy to Thy_Load.load_thy;
wenzelm
parents:
43684
diff
changeset

264 
use "Thy/present.ML"; 
3c2c912af2ef
moved Outer_Syntax.load_thy to Thy_Load.load_thy;
wenzelm
parents:
43684
diff
changeset

265 
use "Thy/thy_load.ML"; 
31432
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

266 
use "Thy/thy_info.ML"; 
44185  267 
use "PIDE/document.ML"; 
42504
869c3f6f2d6e
railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
42405
diff
changeset

268 
use "Thy/rail.ML"; 
31432
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

269 

9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

270 
(*theory and proof operations*) 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

271 
use "Isar/rule_insts.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

272 
use "Thy/thm_deps.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

273 
use "Isar/isar_cmd.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

274 

20207  275 
use "subgoal.ML"; 
5834  276 

13402  277 
use "Proof/extraction.ML"; 
11511  278 

31432
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

279 

9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

280 
(* Isabelle/Isar system *) 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

281 

30173
eabece26b89b
moved isabelle_process.ML, isabelle_process.scala, isar.ML, session.ML to Pure/System/ (together with associated Isar commands);
wenzelm
parents:
29269
diff
changeset

282 
use "System/session.ML"; 
48681
181b91e1d1c1
prefer general Command_Line.tool wrapper (cf. Scala version);
wenzelm
parents:
48646
diff
changeset

283 
use "System/command_line.ML"; 
45029
63144ea111f7
abstract System_Channel in ML (cf. Scala version);
wenzelm
parents:
45026
diff
changeset

284 
use "System/system_channel.ML"; 
38412
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/  sidebyside with isar.ML;
wenzelm
parents:
38379
diff
changeset

285 
use "System/isabelle_process.ML"; 
43748  286 
use "System/invoke_scala.ML"; 
45709
87017fcbad83
clarified modules (again)  NB: both Document and Protocol are specific to this particular prover;
wenzelm
parents:
45672
diff
changeset

287 
use "PIDE/protocol.ML"; 
30173
eabece26b89b
moved isabelle_process.ML, isabelle_process.scala, isar.ML, session.ML to Pure/System/ (together with associated Isar commands);
wenzelm
parents:
29269
diff
changeset

288 
use "System/isar.ML"; 
eabece26b89b
moved isabelle_process.ML, isabelle_process.scala, isar.ML, session.ML to Pure/System/ (together with associated Isar commands);
wenzelm
parents:
29269
diff
changeset

289 

31432
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

290 

9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

291 
(* miscellaneous tools and packages for Pure Isabelle *) 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

292 

50686  293 
use "Tools/build.ML"; 
31432
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

294 
use "Tools/named_thms.ML"; 
50217
ce1f0602f48e
clarified status of Legacy_XML_Syntax, despite lack of Proofterm_XML;
wenzelm
parents:
50201
diff
changeset

295 
use "Tools/legacy_xml_syntax.ML"; 
31432
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

296 

9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

297 

9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

298 
(* configuration for Proof General *) 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

299 

9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

300 
use "ProofGeneral/pgip_types.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

301 
use "ProofGeneral/pgml.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

302 
use "ProofGeneral/pgip_markup.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

303 
use "ProofGeneral/pgip_input.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

304 
use "ProofGeneral/pgip_output.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

305 

9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

306 
use "ProofGeneral/pgip_isabelle.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

307 

50757
37091451ba1a
slightly odd duplication of Pure options for Proof General (amending cb5cdbb645cd);
wenzelm
parents:
50686
diff
changeset

308 
(use 
37091451ba1a
slightly odd duplication of Pure options for Proof General (amending cb5cdbb645cd);
wenzelm
parents:
50686
diff
changeset

309 
> Unsynchronized.setmp Proofterm.proofs 0 
37091451ba1a
slightly odd duplication of Pure options for Proof General (amending cb5cdbb645cd);
wenzelm
parents:
50686
diff
changeset

310 
> Unsynchronized.setmp Multithreading.max_threads 0) 
37091451ba1a
slightly odd duplication of Pure options for Proof General (amending cb5cdbb645cd);
wenzelm
parents:
50686
diff
changeset

311 
"ProofGeneral/preferences.ML"; 
31432
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

312 

9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

313 
use "ProofGeneral/pgip_parser.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

314 

9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

315 
use "ProofGeneral/proof_general_pgip.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

316 
use "ProofGeneral/proof_general_emacs.ML"; 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

317 

16781  318 

48732
f04320479ff9
simplified Pure bootstrap  separate pure_setup.ML was required for Alice/ML at some point;
wenzelm
parents:
48681
diff
changeset

319 
(* ML toplevel pretty printing *) 
f04320479ff9
simplified Pure bootstrap  separate pure_setup.ML was required for Alice/ML at some point;
wenzelm
parents:
48681
diff
changeset

320 

f04320479ff9
simplified Pure bootstrap  separate pure_setup.ML was required for Alice/ML at some point;
wenzelm
parents:
48681
diff
changeset

321 
toplevel_pp ["Pretty", "T"] "(fn _: Pretty.T => Pretty.str \"<pretty>\")"; 
f04320479ff9
simplified Pure bootstrap  separate pure_setup.ML was required for Alice/ML at some point;
wenzelm
parents:
48681
diff
changeset

322 
toplevel_pp ["Task_Queue", "task"] "Pretty.str o Task_Queue.str_of_task"; 
f04320479ff9
simplified Pure bootstrap  separate pure_setup.ML was required for Alice/ML at some point;
wenzelm
parents:
48681
diff
changeset

323 
toplevel_pp ["Task_Queue", "group"] "Pretty.str o Task_Queue.str_of_group"; 
f04320479ff9
simplified Pure bootstrap  separate pure_setup.ML was required for Alice/ML at some point;
wenzelm
parents:
48681
diff
changeset

324 
toplevel_pp ["Position", "T"] "Pretty.position"; 
f04320479ff9
simplified Pure bootstrap  separate pure_setup.ML was required for Alice/ML at some point;
wenzelm
parents:
48681
diff
changeset

325 
toplevel_pp ["Binding", "binding"] "Pretty.str o Binding.print"; 
f04320479ff9
simplified Pure bootstrap  separate pure_setup.ML was required for Alice/ML at some point;
wenzelm
parents:
48681
diff
changeset

326 
toplevel_pp ["Thm", "thm"] "Proof_Display.pp_thm"; 
f04320479ff9
simplified Pure bootstrap  separate pure_setup.ML was required for Alice/ML at some point;
wenzelm
parents:
48681
diff
changeset

327 
toplevel_pp ["Thm", "cterm"] "Proof_Display.pp_cterm"; 
f04320479ff9
simplified Pure bootstrap  separate pure_setup.ML was required for Alice/ML at some point;
wenzelm
parents:
48681
diff
changeset

328 
toplevel_pp ["Thm", "ctyp"] "Proof_Display.pp_ctyp"; 
f04320479ff9
simplified Pure bootstrap  separate pure_setup.ML was required for Alice/ML at some point;
wenzelm
parents:
48681
diff
changeset

329 
toplevel_pp ["Context", "theory"] "Context.pretty_thy"; 
f04320479ff9
simplified Pure bootstrap  separate pure_setup.ML was required for Alice/ML at some point;
wenzelm
parents:
48681
diff
changeset

330 
toplevel_pp ["Context", "theory_ref"] "Context.pretty_thy o Theory.deref"; 
f04320479ff9
simplified Pure bootstrap  separate pure_setup.ML was required for Alice/ML at some point;
wenzelm
parents:
48681
diff
changeset

331 
toplevel_pp ["Context", "Proof", "context"] "Proof_Display.pp_context"; 
f04320479ff9
simplified Pure bootstrap  separate pure_setup.ML was required for Alice/ML at some point;
wenzelm
parents:
48681
diff
changeset

332 
toplevel_pp ["Ast", "ast"] "Ast.pretty_ast"; 
f04320479ff9
simplified Pure bootstrap  separate pure_setup.ML was required for Alice/ML at some point;
wenzelm
parents:
48681
diff
changeset

333 
toplevel_pp ["Path", "T"] "Path.pretty"; 
f04320479ff9
simplified Pure bootstrap  separate pure_setup.ML was required for Alice/ML at some point;
wenzelm
parents:
48681
diff
changeset

334 
toplevel_pp ["SHA1", "digest"] "Pretty.str o quote o SHA1.rep"; 
f04320479ff9
simplified Pure bootstrap  separate pure_setup.ML was required for Alice/ML at some point;
wenzelm
parents:
48681
diff
changeset

335 
toplevel_pp ["Proof", "state"] "(fn _: Proof.state => Pretty.str \"<Proof.state>\")"; 
f04320479ff9
simplified Pure bootstrap  separate pure_setup.ML was required for Alice/ML at some point;
wenzelm
parents:
48681
diff
changeset

336 
toplevel_pp ["Toplevel", "state"] "Toplevel.pretty_abstract"; 
f04320479ff9
simplified Pure bootstrap  separate pure_setup.ML was required for Alice/ML at some point;
wenzelm
parents:
48681
diff
changeset

337 

f04320479ff9
simplified Pure bootstrap  separate pure_setup.ML was required for Alice/ML at some point;
wenzelm
parents:
48681
diff
changeset

338 
if ML_System.is_polyml then use "ML/install_pp_polyml.ML" else (); 
f04320479ff9
simplified Pure bootstrap  separate pure_setup.ML was required for Alice/ML at some point;
wenzelm
parents:
48681
diff
changeset

339 

f04320479ff9
simplified Pure bootstrap  separate pure_setup.ML was required for Alice/ML at some point;
wenzelm
parents:
48681
diff
changeset

340 

49862
fb2d8ba7d3a9
more friendly handling of Pure.thy bootstrap errors;
wenzelm
parents:
49561
diff
changeset

341 
(* the Pure theory *) 
fb2d8ba7d3a9
more friendly handling of Pure.thy bootstrap errors;
wenzelm
parents:
49561
diff
changeset

342 

fb2d8ba7d3a9
more friendly handling of Pure.thy bootstrap errors;
wenzelm
parents:
49561
diff
changeset

343 
use "pure_syn.ML"; 
fb2d8ba7d3a9
more friendly handling of Pure.thy bootstrap errors;
wenzelm
parents:
49561
diff
changeset

344 
Toplevel.program (fn () => Thy_Info.use_thy ("Pure", Position.none)); 
fb2d8ba7d3a9
more friendly handling of Pure.thy bootstrap errors;
wenzelm
parents:
49561
diff
changeset

345 
Context.set_thread_data NONE; 
fb2d8ba7d3a9
more friendly handling of Pure.thy bootstrap errors;
wenzelm
parents:
49561
diff
changeset

346 
structure Pure = struct val thy = Thy_Info.get_theory "Pure" end; 
fb2d8ba7d3a9
more friendly handling of Pure.thy bootstrap errors;
wenzelm
parents:
49561
diff
changeset

347 

fb2d8ba7d3a9
more friendly handling of Pure.thy bootstrap errors;
wenzelm
parents:
49561
diff
changeset

348 
toplevel_pp ["typ"] "Proof_Display.pp_typ Pure.thy"; 
fb2d8ba7d3a9
more friendly handling of Pure.thy bootstrap errors;
wenzelm
parents:
49561
diff
changeset

349 

fb2d8ba7d3a9
more friendly handling of Pure.thy bootstrap errors;
wenzelm
parents:
49561
diff
changeset

350 

48879  351 
(* ML toplevel commands *) 
352 

353 
fun use name = Toplevel.program (fn () => Thy_Load.use_ml (Path.explode name)); 

354 

48927
ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48879
diff
changeset

355 
fun use_thys args = Toplevel.program (fn () => Thy_Info.use_thys (map (rpair Position.none) args)); 
ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48879
diff
changeset

356 
val use_thy = use_thys o single; 
48732
f04320479ff9
simplified Pure bootstrap  separate pure_setup.ML was required for Alice/ML at some point;
wenzelm
parents:
48681
diff
changeset

357 

f04320479ff9
simplified Pure bootstrap  separate pure_setup.ML was required for Alice/ML at some point;
wenzelm
parents:
48681
diff
changeset

358 
val cd = File.cd o Path.explode; 
f04320479ff9
simplified Pure bootstrap  separate pure_setup.ML was required for Alice/ML at some point;
wenzelm
parents:
48681
diff
changeset

359 

f04320479ff9
simplified Pure bootstrap  separate pure_setup.ML was required for Alice/ML at some point;
wenzelm
parents:
48681
diff
changeset

360 
Proofterm.proofs := 0; 
48879  361 
Multithreading.max_threads := 0; 
30639
fe40d740d7c1
ML/ml_test.ML: test of advanced ML compiler invocation in Poly/ML 5.3;
wenzelm
parents:
30559
diff
changeset

362 