author  wenzelm 
Thu, 17 Mar 2016 10:21:43 +0100  
changeset 62657  cdd6db02eae8 
parent 62643  6f7ac44365d7 
child 62658  c27dabf438d6 
permissions  rwrr 
62643  1 
(*** Isabelle/Pure bootstrap ***) 
62508
d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62501
diff
changeset

2 

d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62501
diff
changeset

3 
(** bootstrap phase 0: Poly/ML setup **) 
d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62501
diff
changeset

4 

d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62501
diff
changeset

5 
(* initial ML name space *) 
56288  6 

62508
d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62501
diff
changeset

7 
use "ML/ml_system.ML"; 
d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62501
diff
changeset

8 
use "ML/ml_name_space.ML"; 
d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62501
diff
changeset

9 

d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62501
diff
changeset

10 
if List.exists (fn (a, _) => a = "FixedInt") (#allStruct ML_Name_Space.global ()) then () 
d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62501
diff
changeset

11 
else use "ML/fixed_int_dummy.ML"; 
0  12 

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

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

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

15 
val version = "unidentified repository version"; 
57649
a43898f76ae9
further distinction of Isabelle distribution: alert for identified release candidates;
wenzelm
parents:
56438
diff
changeset

16 
val is_identified = false; 
27642
c0db1220b071
structure Distribution: swapped default for is_official;
wenzelm
parents:
27546
diff
changeset

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

18 
end; 
11835  19 

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

20 

62508
d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62501
diff
changeset

21 
(* multithreading *) 
d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62501
diff
changeset

22 

d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62501
diff
changeset

23 
use "General/exn.ML"; 
d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62501
diff
changeset

24 

d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62501
diff
changeset

25 
val seconds = Time.fromReal; 
d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62501
diff
changeset

26 

d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62501
diff
changeset

27 
open Thread; 
d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62501
diff
changeset

28 
use "Concurrent/multithreading.ML"; 
d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62501
diff
changeset

29 

d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62501
diff
changeset

30 
use "Concurrent/unsynchronized.ML"; 
62657  31 
val _ = ML_Name_Space.forget_val "ref"; 
32 
val _ = ML_Name_Space.forget_type "ref"; 

62508
d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62501
diff
changeset

33 

d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62501
diff
changeset

34 

d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62501
diff
changeset

35 
(* pervasive environment *) 
d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62501
diff
changeset

36 

62657  37 
val _ = ML_Name_Space.forget_val "isSome"; 
38 
val _ = ML_Name_Space.forget_val "getOpt"; 

39 
val _ = ML_Name_Space.forget_val "valOf"; 

40 
val _ = ML_Name_Space.forget_val "foldl"; 

41 
val _ = ML_Name_Space.forget_val "foldr"; 

42 
val _ = ML_Name_Space.forget_val "print"; 

43 
val _ = ML_Name_Space.forget_val "explode"; 

44 
val _ = ML_Name_Space.forget_val "concat"; 

62508
d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62501
diff
changeset

45 

d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62501
diff
changeset

46 
val ord = SML90.ord; 
d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62501
diff
changeset

47 
val chr = SML90.chr; 
d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62501
diff
changeset

48 
val raw_explode = SML90.explode; 
d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62501
diff
changeset

49 
val implode = SML90.implode; 
d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62501
diff
changeset

50 

d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62501
diff
changeset

51 
fun quit () = exit 0; 
d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62501
diff
changeset

52 

d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62501
diff
changeset

53 

d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62501
diff
changeset

54 
(* ML runtime system *) 
d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62501
diff
changeset

55 

d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62501
diff
changeset

56 
use "ML/ml_heap.ML"; 
d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62501
diff
changeset

57 
use "ML/ml_profiling.ML"; 
d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62501
diff
changeset

58 

d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62501
diff
changeset

59 
val pointer_eq = PolyML.pointerEq; 
d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62501
diff
changeset

60 

d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62501
diff
changeset

61 

d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62501
diff
changeset

62 
(* ML toplevel pretty printing *) 
d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62501
diff
changeset

63 

d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62501
diff
changeset

64 
use "ML/ml_pretty.ML"; 
d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62501
diff
changeset

65 

d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62501
diff
changeset

66 
local 
d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62501
diff
changeset

67 
val depth = Unsynchronized.ref 10; 
d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62501
diff
changeset

68 
in 
d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62501
diff
changeset

69 
fun get_default_print_depth () = ! depth; 
d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62501
diff
changeset

70 
fun default_print_depth n = (depth := n; PolyML.print_depth n); 
d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62501
diff
changeset

71 
val _ = default_print_depth 10; 
d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62501
diff
changeset

72 
end; 
d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62501
diff
changeset

73 

d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62501
diff
changeset

74 
val error_depth = PolyML.error_depth; 
d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62501
diff
changeset

75 

d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62501
diff
changeset

76 

d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62501
diff
changeset

77 
(* ML compiler *) 
d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62501
diff
changeset

78 

d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62501
diff
changeset

79 
use "General/secure.ML"; 
d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62501
diff
changeset

80 
use "ML/ml_compiler0.ML"; 
d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62501
diff
changeset

81 

d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62501
diff
changeset

82 
PolyML.Compiler.reportUnreferencedIds := true; 
d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62501
diff
changeset

83 
PolyML.Compiler.reportExhaustiveHandlers := true; 
d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62501
diff
changeset

84 
PolyML.Compiler.printInAlphabeticalOrder := false; 
d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62501
diff
changeset

85 
PolyML.Compiler.maxInlineSize := 80; 
d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62501
diff
changeset

86 

d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62501
diff
changeset

87 
fun ml_make_string struct_name = 
d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62501
diff
changeset

88 
"(fn x => Pretty.string_of (Pretty.from_ML (ML_Pretty.from_polyml (PolyML.prettyRepresentation (x, FixedInt.fromInt (" ^ 
d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62501
diff
changeset

89 
struct_name ^ ".ML_print_depth ()))))))"; 
d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62501
diff
changeset

90 

d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62501
diff
changeset

91 

d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62501
diff
changeset

92 
(* ML debugger *) 
d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62501
diff
changeset

93 

d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62501
diff
changeset

94 
use_no_debug "ML/ml_debugger.ML"; 
d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62501
diff
changeset

95 

d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62501
diff
changeset

96 

d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62501
diff
changeset

97 

d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62501
diff
changeset

98 
(** bootstrap phase 1: towards ML within position context *) 
d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62501
diff
changeset

99 

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

100 
(* 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

101 

21396  102 
use "General/basics.ML"; 
0  103 
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

104 
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

105 
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

106 
use "General/table.ML"; 
43684  107 

108 
use "Concurrent/synchronized.ML"; 

52537  109 
use "Concurrent/counter.ML"; 
43684  110 

62585  111 
use "General/random.ML"; 
43746
a41f618c641d
some support for raw messages, which bypass standard Symbol/YXML decoding;
wenzelm
parents:
43729
diff
changeset

112 
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

113 
use "General/output.ML"; 
45670  114 
use "PIDE/markup.ML"; 
31432
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

115 
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

116 
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

117 
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

118 
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

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

121 
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

122 
use "ML/ml_lex.ML"; 
56288  123 

62493  124 
val {use, use_debug, use_no_debug} = 
125 
let 

62494  126 
val context: ML_Compiler0.context = 
62493  127 
{name_space = ML_Name_Space.global, 
128 
here = Position.here oo Position.line_file, 

129 
print = writeln, 

62494  130 
error = error}; 
62493  131 
in 
62494  132 
ML_Compiler0.use_operations (fn opt_debug => fn file => 
62493  133 
Position.setmp_thread_data (Position.file_only file) 
134 
(fn () => 

62494  135 
ML_Compiler0.use_file context 
136 
{verbose = true, debug = ML_Compiler0.debug_option opt_debug} file 

137 
handle ERROR msg => (writeln msg; error "ML error")) ()) 

62493  138 
end; 
56434  139 

56288  140 

59054
61b723761dff
load simple_thread.ML later, such that it benefits from redefined print_exception_trace;
wenzelm
parents:
59026
diff
changeset

141 

62508
d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62501
diff
changeset

142 
(** bootstrap phase 2: towards ML within Isar context *) 
56288  143 

144 
(* library of general tools *) 

145 

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

146 
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

147 
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

148 
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

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

150 
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

151 
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

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

153 
use "General/linear_set.ML"; 
43593  154 
use "General/buffer.ML"; 
43791  155 
use "General/pretty.ML"; 
59363
4660b0409096
added Path.decode in ML, in correspondence to Path.encode in Scala;
wenzelm
parents:
59203
diff
changeset

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

157 
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

158 
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

159 
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

160 
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

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

162 
use "General/socket_io.ML"; 
56287  163 
use "General/seq.ML"; 
164 
use "General/timing.ML"; 

22592  165 

35628  166 
use "General/sha1.ML"; 
62354  167 
use "General/sha1_polyml.ML"; 
53212
387b9f7cb0ac
added SHA1 library integrity test, which is invoked at compile time and Isabelle_Process runtime;
wenzelm
parents:
53192
diff
changeset

168 
use "General/sha1_samples.ML"; 
35628  169 

44698  170 
use "PIDE/yxml.ML"; 
56303
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
56288
diff
changeset

171 
use "PIDE/document_id.ML"; 
44698  172 

56053
030531cc4c62
tables with changes relative to some common base version  support for efficient join/merge of big global tables with small local updates;
wenzelm
parents:
55672
diff
changeset

173 
use "General/change_table.ML"; 
49560  174 
use "General/graph.ML"; 
175 

60911
858694df711b
default ML context for forks, e.g. relevant for debugging and toplevel prettyprinting;
wenzelm
parents:
60630
diff
changeset

176 

858694df711b
default ML context for forks, e.g. relevant for debugging and toplevel prettyprinting;
wenzelm
parents:
60630
diff
changeset

177 
(* fundamental structures *) 
858694df711b
default ML context for forks, e.g. relevant for debugging and toplevel prettyprinting;
wenzelm
parents:
60630
diff
changeset

178 

858694df711b
default ML context for forks, e.g. relevant for debugging and toplevel prettyprinting;
wenzelm
parents:
60630
diff
changeset

179 
use "name.ML"; 
858694df711b
default ML context for forks, e.g. relevant for debugging and toplevel prettyprinting;
wenzelm
parents:
60630
diff
changeset

180 
use "term.ML"; 
858694df711b
default ML context for forks, e.g. relevant for debugging and toplevel prettyprinting;
wenzelm
parents:
60630
diff
changeset

181 
use "context.ML"; 
858694df711b
default ML context for forks, e.g. relevant for debugging and toplevel prettyprinting;
wenzelm
parents:
60630
diff
changeset

182 
use "context_position.ML"; 
51947
3301612c4893
support for system options as contextsensitive config options;
wenzelm
parents:
51933
diff
changeset

183 
use "System/options.ML"; 
60911
858694df711b
default ML context for forks, e.g. relevant for debugging and toplevel prettyprinting;
wenzelm
parents:
60630
diff
changeset

184 
use "config.ML"; 
51947
3301612c4893
support for system options as contextsensitive config options;
wenzelm
parents:
51933
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 

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

187 
(* concurrency within the ML runtime *) 
28120  188 

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

190 

62501  191 
use "ML/ml_statistics.ML"; 
50255  192 

61556  193 
use "Concurrent/standard_thread.ML"; 
62359  194 
use "Concurrent/single_assignment.ML"; 
59054
61b723761dff
load simple_thread.ML later, such that it benefits from redefined print_exception_trace;
wenzelm
parents:
59026
diff
changeset

195 

44247  196 
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

197 
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

198 
use "Concurrent/future.ML"; 
52798
9d3c9862d1dd
recovered delay for Document.start_execution (see also 627fb639a2d9), which potentially improves throughput when many consecutive edits arrive;
wenzelm
parents:
52788
diff
changeset

199 
use "Concurrent/event_timer.ML"; 
62519  200 
use "Concurrent/timeout.ML"; 
32815
1a5e364584ae
separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents:
32738
diff
changeset

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

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

203 

44247  204 
use "Concurrent/mailbox.ML"; 
32840  205 
use "Concurrent/cache.ML"; 
206 

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

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

208 

31432
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 
(* inner syntax *) 
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

211 

52211
66bc827e37f8
explicit support for type annotations within printed syntax trees;
wenzelm
parents:
52140
diff
changeset

212 
use "Syntax/type_annotation.ML"; 
42264  213 
use "Syntax/term_position.ML"; 
214 
use "Syntax/lexicon.ML"; 

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

216 
use "Syntax/syntax_ext.ML"; 
22679  217 
use "Syntax/parser.ML"; 
42284  218 
use "Syntax/syntax_trans.ML"; 
22679  219 
use "Syntax/mixfix.ML"; 
220 
use "Syntax/printer.ML"; 

221 
use "Syntax/syntax.ML"; 

222 

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

223 

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

224 
(* 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

225 

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

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

227 
use "term_subst.ML"; 
43729  228 
use "term_xml.ML"; 
55672
5e25cc741ab9
support for completion within the formal context;
wenzelm
parents:
55516
diff
changeset

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

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

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

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

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

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

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

236 
use "item_net.ML"; 
18934  237 
use "envir.ML"; 
18059  238 
use "consts.ML"; 
24257  239 
use "primitive_defs.ML"; 
61261
ddb2da7cb2e4
more explicit Defs.context: use proper name spaces as far as possible;
wenzelm
parents:
60962
diff
changeset

240 
use "sign.ML"; 
27546  241 
use "defs.ML"; 
43795
ca5896a836ba
recovered some runtime sharing from d6b6c74a8bcf, without the global memory bottleneck;
wenzelm
parents:
43794
diff
changeset

242 
use "term_sharing.ML"; 
0  243 
use "pattern.ML"; 
244 
use "unify.ML"; 

1528  245 
use "theory.ML"; 
11511  246 
use "proofterm.ML"; 
0  247 
use "thm.ML"; 
59026
30b8a5825a9c
removed some addons from modules that are relevant for the inference kernel;
wenzelm
parents:
58928
diff
changeset

248 
use "more_pattern.ML"; 
30b8a5825a9c
removed some addons from modules that are relevant for the inference kernel;
wenzelm
parents:
58928
diff
changeset

249 
use "more_unify.ML"; 
22361  250 
use "more_thm.ML"; 
26279  251 
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

252 
use "global_theory.ML"; 
3986  253 
use "pure_thy.ML"; 
0  254 
use "drule.ML"; 
22233  255 
use "morphism.ML"; 
19898  256 
use "variable.ML"; 
24833  257 
use "conv.ML"; 
32187  258 
use "goal_display.ML"; 
32169  259 
use "tactical.ML"; 
1582  260 
use "search.ML"; 
21708  261 
use "tactic.ML"; 
41228
e1fce873b814
renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
wenzelm
parents:
40748
diff
changeset

262 
use "raw_simplifier.ML"; 
19417  263 
use "conjunction.ML"; 
20225  264 
use "assumption.ML"; 
0  265 

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

266 

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

267 
(* 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

268 

56303
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
56288
diff
changeset

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

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

271 
use "ML/ml_env.ML"; 
56303
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
56288
diff
changeset

272 
use "ML/ml_options.ML"; 
62498  273 
use_no_debug "ML/exn_debugger.ML"; 
56303
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
56288
diff
changeset

274 
use "ML/ml_options.ML"; 
62498  275 
use_no_debug "Isar/runtime.ML"; 
56303
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
56288
diff
changeset

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

278 

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

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

281 

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

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

283 
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

284 
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

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

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

287 
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

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

289 
use "type_infer_context.ML"; 
42243  290 
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

291 
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

292 

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

293 
(*outer syntax*) 
58903  294 
use "Isar/keyword.ML"; 
36959
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
36955
diff
changeset

295 
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

296 
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

297 
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

298 

57926
59b2572e8e93
load local_theory.ML before attrib.ML, with subtle change of semantics due to canonical Local_Theory.map_contexts instead of private Local_Theory.map_top;
wenzelm
parents:
57905
diff
changeset

299 
(*theory specifications*) 
59b2572e8e93
load local_theory.ML before attrib.ML, with subtle change of semantics due to canonical Local_Theory.map_contexts instead of private Local_Theory.map_top;
wenzelm
parents:
57905
diff
changeset

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

301 
use "Thy/thy_header.ML"; 
57905
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
57649
diff
changeset

302 
use "PIDE/command_span.ML"; 
51265  303 
use "Thy/thy_syntax.ML"; 
61454  304 
use "Thy/markdown.ML"; 
31432
9858f32f9569
just one ROOT.ML without any cd or ".."  simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset

305 
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

306 
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

307 

56203
76c72f4d0667
clarified bootstrap process: switch to ML with context and antiquotations earlier;
wenzelm
parents:
56072
diff
changeset

308 
(*ML with context and antiquotations*) 
76c72f4d0667
clarified bootstrap process: switch to ML with context and antiquotations earlier;
wenzelm
parents:
56072
diff
changeset

309 
use "ML/ml_context.ML"; 
56205  310 
use "ML/ml_antiquotation.ML"; 
56288  311 

62493  312 
val {use, use_debug, use_no_debug} = 
62494  313 
ML_Compiler0.use_operations (fn opt_debug => fn file => 
62493  314 
let val flags = ML_Compiler.verbose true (ML_Compiler.debug_flags opt_debug) in 
62490
39d01eaf5292
ML debugger support in Pure (again, see 3565c9f407ec);
wenzelm
parents:
62459
diff
changeset

315 
ML_Context.eval_file flags (Path.explode file) 
39d01eaf5292
ML debugger support in Pure (again, see 3565c9f407ec);
wenzelm
parents:
62459
diff
changeset

316 
handle ERROR msg => (writeln msg; error "ML error") 
62493  317 
end); 
56434  318 

56288  319 

320 

62508
d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62501
diff
changeset

321 
(** bootstrap phase 3: towards Pure.thy and final ML toplevel setup *) 
56203
76c72f4d0667
clarified bootstrap process: switch to ML with context and antiquotations earlier;
wenzelm
parents:
56072
diff
changeset

322 

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

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

325 
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

326 
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

327 
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

328 
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

329 
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

330 
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

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

333 

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

334 
(*local theories and targets*) 
52140  335 
use "Isar/locale.ML"; 
38307
0028571ade2d
split off structure Generic_Target into separate file
haftmann
parents:
38150
diff
changeset

336 
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

337 
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

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

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

340 
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

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

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

346 

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

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

349 

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

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

351 
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

352 

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

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

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

355 
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

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

358 

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

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

360 
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

361 
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

362 

56206  363 
(*proof term operations*) 
364 
use "Proof/reconstruct.ML"; 

365 
use "Proof/proof_syntax.ML"; 

366 
use "Proof/proof_rewrite_rules.ML"; 

367 
use "Proof/proof_checker.ML"; 

368 
use "Proof/extraction.ML"; 

369 

62584  370 
(*Isabelle system*) 
371 
if ML_System.platform_is_windows 

372 
then use "System/bash_windows.ML" 

373 
else use "System/bash.ML"; 

374 
use "System/isabelle_system.ML"; 

375 

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

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

377 
use "Thy/term_style.ML"; 
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58903
diff
changeset

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

379 
use "Thy/thy_output.ML"; 
61619  380 
use "Thy/document_antiquotations.ML"; 
49561  381 
use "General/graph_display.ML"; 
43712
3c2c912af2ef
moved Outer_Syntax.load_thy to Thy_Load.load_thy;
wenzelm
parents:
43684
diff
changeset

382 
use "Thy/present.ML"; 
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58903
diff
changeset

383 
use "pure_syn.ML"; 
52510  384 
use "PIDE/command.ML"; 
52865
02a7e7180ee5
slightly more general support for oneshot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
52836
diff
changeset

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

387 
use "Thy/thy_info.ML"; 
59086
94b2690ad494
nodespecific keywords, with session base syntax as default;
wenzelm
parents:
59064
diff
changeset

388 
use "PIDE/session.ML"; 
59714
ae322325adbb
tuned protocol  resolve command positions in ML;
wenzelm
parents:
59470
diff
changeset

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

391 

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

392 
(*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

393 
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

394 

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

395 

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

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

397 

48681
181b91e1d1c1
prefer general Command_Line.tool wrapper (cf. Scala version);
wenzelm
parents:
48646
diff
changeset

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

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

401 
use "System/isabelle_process.ML"; 
43748  402 
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

403 
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

404 

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

405 

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

406 
(* 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

407 

50686  408 
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

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

410 

55387
51f0876f61df
seal system channels at end of Pure bootstrap  Isabelle/Scala provides official interfaces;
wenzelm
parents:
55141
diff
changeset

411 
structure Output: OUTPUT = Output; (*seal system channels!*) 
51f0876f61df
seal system channels at end of Pure bootstrap  Isabelle/Scala provides official interfaces;
wenzelm
parents:
55141
diff
changeset

412 

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

413 

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

415 

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

416 

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

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

418 

58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58903
diff
changeset

419 
use "ML/ml_file.ML"; 
56303
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
56288
diff
changeset

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

421 
Context.set_thread_data NONE; 
60937  422 
structure Pure = struct val thy = Thy_Info.pure_theory () end; 
49862
fb2d8ba7d3a9
more friendly handling of Pure.thy bootstrap errors;
wenzelm
parents:
49561
diff
changeset

423 

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

424 

48879  425 
(* ML toplevel commands *) 
426 

56303
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
56288
diff
changeset

427 
fun use_thys args = 
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
56288
diff
changeset

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

429 
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

430 

52487
48bc24467008
backout dedd7952a62c: static "proofs" value within theory prevents later inferencing with different configuration;
wenzelm
parents:
52470
diff
changeset

431 
Proofterm.proofs := 0; 