author | wenzelm |
Wed, 06 Apr 2016 19:03:29 +0200 | |
changeset 62893 | fca40adc6342 |
parent 62890 | 728aa05e9433 |
child 62896 | 4ee9c2be4383 |
permissions | -rw-r--r-- |
62643 | 1 |
(*** Isabelle/Pure bootstrap ***) |
62508
d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62501
diff
changeset
|
2 |
|
62883 | 3 |
use "ML/ml_name_space.ML"; |
4 |
||
5 |
||
62508
d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62501
diff
changeset
|
6 |
(** bootstrap phase 0: Poly/ML setup **) |
d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62501
diff
changeset
|
7 |
|
62883 | 8 |
use "ML/ml_pervasive0.ML"; |
62853 | 9 |
use "ML/ml_system.ML"; |
62883 | 10 |
use "System/distribution.ML"; |
62508
d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62501
diff
changeset
|
11 |
|
d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62501
diff
changeset
|
12 |
use "General/exn.ML"; |
d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62501
diff
changeset
|
13 |
|
d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62501
diff
changeset
|
14 |
use "Concurrent/multithreading.ML"; |
d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62501
diff
changeset
|
15 |
use "Concurrent/unsynchronized.ML"; |
d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62501
diff
changeset
|
16 |
|
d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62501
diff
changeset
|
17 |
use "ML/ml_heap.ML"; |
d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62501
diff
changeset
|
18 |
use "ML/ml_profiling.ML"; |
62878 | 19 |
use "ML/ml_print_depth0.ML"; |
62508
d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62501
diff
changeset
|
20 |
use "ML/ml_pretty.ML"; |
d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62501
diff
changeset
|
21 |
use "ML/ml_compiler0.ML"; |
d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62501
diff
changeset
|
22 |
use_no_debug "ML/ml_debugger.ML"; |
d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62501
diff
changeset
|
23 |
|
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 |
|
d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62501
diff
changeset
|
26 |
(** 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
|
27 |
|
31432
9858f32f9569
just one ROOT.ML without any cd or ".." -- simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset
|
28 |
(* 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
|
29 |
|
21396 | 30 |
use "General/basics.ML"; |
0 | 31 |
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
|
32 |
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
|
33 |
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
|
34 |
use "General/table.ML"; |
43684 | 35 |
|
36 |
use "Concurrent/synchronized.ML"; |
|
52537 | 37 |
use "Concurrent/counter.ML"; |
43684 | 38 |
|
62585 | 39 |
use "General/random.ML"; |
43746
a41f618c641d
some support for raw messages, which bypass standard Symbol/YXML decoding;
wenzelm
parents:
43729
diff
changeset
|
40 |
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
|
41 |
use "General/output.ML"; |
45670 | 42 |
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
|
43 |
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
|
44 |
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
|
45 |
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
|
46 |
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
|
47 |
use "General/symbol_pos.ML"; |
59064 | 48 |
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
|
49 |
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
|
50 |
use "ML/ml_lex.ML"; |
62817 | 51 |
use "ML/ml_compiler1.ML"; |
56288 | 52 |
|
59054
61b723761dff
load simple_thread.ML later, such that it benefits from redefined print_exception_trace;
wenzelm
parents:
59026
diff
changeset
|
53 |
|
62508
d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62501
diff
changeset
|
54 |
(** bootstrap phase 2: towards ML within Isar context *) |
56288 | 55 |
|
56 |
(* library of general tools *) |
|
57 |
||
31432
9858f32f9569
just one ROOT.ML without any cd or ".." -- simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset
|
58 |
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
|
59 |
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
|
60 |
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
|
61 |
use "General/heap.ML"; |
32015
7101feb5247e
Support for copy-avoiding functions on pure values, at the cost of readability.
wenzelm
parents:
31476
diff
changeset
|
62 |
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
|
63 |
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
|
64 |
use "General/balanced_tree.ML"; |
38448
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38418
diff
changeset
|
65 |
use "General/linear_set.ML"; |
43593 | 66 |
use "General/buffer.ML"; |
43791 | 67 |
use "General/pretty.ML"; |
59363
4660b0409096
added Path.decode in ML, in correspondence to Path.encode in Scala;
wenzelm
parents:
59203
diff
changeset
|
68 |
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
|
69 |
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
|
70 |
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
|
71 |
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
|
72 |
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
|
73 |
use "General/binding.ML"; |
50800
c0fb2839d1a9
recovered buffered sockets from 11f622794ad6 -- requires Poly/ML 5.5.x;
wenzelm
parents:
50757
diff
changeset
|
74 |
use "General/socket_io.ML"; |
56287 | 75 |
use "General/seq.ML"; |
76 |
use "General/timing.ML"; |
|
35628 | 77 |
use "General/sha1.ML"; |
78 |
||
44698 | 79 |
use "PIDE/yxml.ML"; |
56303
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
56288
diff
changeset
|
80 |
use "PIDE/document_id.ML"; |
44698 | 81 |
|
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
|
82 |
use "General/change_table.ML"; |
49560 | 83 |
use "General/graph.ML"; |
84 |
||
60911
858694df711b
default ML context for forks, e.g. relevant for debugging and toplevel pretty-printing;
wenzelm
parents:
60630
diff
changeset
|
85 |
|
858694df711b
default ML context for forks, e.g. relevant for debugging and toplevel pretty-printing;
wenzelm
parents:
60630
diff
changeset
|
86 |
(* fundamental structures *) |
858694df711b
default ML context for forks, e.g. relevant for debugging and toplevel pretty-printing;
wenzelm
parents:
60630
diff
changeset
|
87 |
|
858694df711b
default ML context for forks, e.g. relevant for debugging and toplevel pretty-printing;
wenzelm
parents:
60630
diff
changeset
|
88 |
use "name.ML"; |
858694df711b
default ML context for forks, e.g. relevant for debugging and toplevel pretty-printing;
wenzelm
parents:
60630
diff
changeset
|
89 |
use "term.ML"; |
858694df711b
default ML context for forks, e.g. relevant for debugging and toplevel pretty-printing;
wenzelm
parents:
60630
diff
changeset
|
90 |
use "context.ML"; |
858694df711b
default ML context for forks, e.g. relevant for debugging and toplevel pretty-printing;
wenzelm
parents:
60630
diff
changeset
|
91 |
use "context_position.ML"; |
51947
3301612c4893
support for system options as context-sensitive config options;
wenzelm
parents:
51933
diff
changeset
|
92 |
use "System/options.ML"; |
60911
858694df711b
default ML context for forks, e.g. relevant for debugging and toplevel pretty-printing;
wenzelm
parents:
60630
diff
changeset
|
93 |
use "config.ML"; |
51947
3301612c4893
support for system options as context-sensitive config options;
wenzelm
parents:
51933
diff
changeset
|
94 |
|
31432
9858f32f9569
just one ROOT.ML without any cd or ".." -- simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset
|
95 |
|
9858f32f9569
just one ROOT.ML without any cd or ".." -- simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset
|
96 |
(* concurrency within the ML runtime *) |
28120 | 97 |
|
62355 | 98 |
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
|
99 |
|
62501 | 100 |
use "ML/ml_statistics.ML"; |
50255 | 101 |
|
62893
fca40adc6342
virtual thread data via context, for proper support of Context.>> etc;
wenzelm
parents:
62890
diff
changeset
|
102 |
use "Concurrent/thread_data_virtual.ML"; |
61556 | 103 |
use "Concurrent/standard_thread.ML"; |
62359 | 104 |
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
|
105 |
|
44247 | 106 |
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
|
107 |
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
|
108 |
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
|
109 |
use "Concurrent/event_timer.ML"; |
62519 | 110 |
use "Concurrent/timeout.ML"; |
32815
1a5e364584ae
separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents:
32738
diff
changeset
|
111 |
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
|
112 |
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
|
113 |
|
44247 | 114 |
use "Concurrent/mailbox.ML"; |
32840 | 115 |
use "Concurrent/cache.ML"; |
116 |
||
50500
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
117 |
use "PIDE/active.ML"; |
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
118 |
|
31432
9858f32f9569
just one ROOT.ML without any cd or ".." -- simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset
|
119 |
|
9858f32f9569
just one ROOT.ML without any cd or ".." -- simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset
|
120 |
(* inner syntax *) |
9858f32f9569
just one ROOT.ML without any cd or ".." -- simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset
|
121 |
|
52211
66bc827e37f8
explicit support for type annotations within printed syntax trees;
wenzelm
parents:
52140
diff
changeset
|
122 |
use "Syntax/type_annotation.ML"; |
42264 | 123 |
use "Syntax/term_position.ML"; |
124 |
use "Syntax/lexicon.ML"; |
|
22679 | 125 |
use "Syntax/ast.ML"; |
42288
2074b31650e6
discontinued special treatment of structure Syntax_Ext (formerly Syn_Ext);
wenzelm
parents:
42284
diff
changeset
|
126 |
use "Syntax/syntax_ext.ML"; |
22679 | 127 |
use "Syntax/parser.ML"; |
42284 | 128 |
use "Syntax/syntax_trans.ML"; |
22679 | 129 |
use "Syntax/mixfix.ML"; |
130 |
use "Syntax/printer.ML"; |
|
131 |
use "Syntax/syntax.ML"; |
|
132 |
||
31432
9858f32f9569
just one ROOT.ML without any cd or ".." -- simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset
|
133 |
|
9858f32f9569
just one ROOT.ML without any cd or ".." -- simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset
|
134 |
(* 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
|
135 |
|
42382
dcd983ee2c29
provide structure Syntax early (before structure Type), back-patch check/uncheck later;
wenzelm
parents:
42357
diff
changeset
|
136 |
use "term_ord.ML"; |
dcd983ee2c29
provide structure Syntax early (before structure Type), back-patch check/uncheck later;
wenzelm
parents:
42357
diff
changeset
|
137 |
use "term_subst.ML"; |
43729 | 138 |
use "term_xml.ML"; |
55672
5e25cc741ab9
support for completion within the formal context;
wenzelm
parents:
55516
diff
changeset
|
139 |
use "General/completion.ML"; |
42382
dcd983ee2c29
provide structure Syntax early (before structure Type), back-patch check/uncheck later;
wenzelm
parents:
42357
diff
changeset
|
140 |
use "General/name_space.ML"; |
dcd983ee2c29
provide structure Syntax early (before structure Type), back-patch check/uncheck later;
wenzelm
parents:
42357
diff
changeset
|
141 |
use "sorts.ML"; |
dcd983ee2c29
provide structure Syntax early (before structure Type), back-patch check/uncheck later;
wenzelm
parents:
42357
diff
changeset
|
142 |
use "type.ML"; |
dcd983ee2c29
provide structure Syntax early (before structure Type), back-patch check/uncheck later;
wenzelm
parents:
42357
diff
changeset
|
143 |
use "logic.ML"; |
dcd983ee2c29
provide structure Syntax early (before structure Type), back-patch check/uncheck later;
wenzelm
parents:
42357
diff
changeset
|
144 |
use "Syntax/simple_syntax.ML"; |
30559
e5987a7ac5df
turned structure NetRules into general Item_Net, which is loaded earlier;
wenzelm
parents:
30173
diff
changeset
|
145 |
use "net.ML"; |
e5987a7ac5df
turned structure NetRules into general Item_Net, which is loaded earlier;
wenzelm
parents:
30173
diff
changeset
|
146 |
use "item_net.ML"; |
18934 | 147 |
use "envir.ML"; |
18059 | 148 |
use "consts.ML"; |
24257 | 149 |
use "primitive_defs.ML"; |
61261
ddb2da7cb2e4
more explicit Defs.context: use proper name spaces as far as possible;
wenzelm
parents:
60962
diff
changeset
|
150 |
use "sign.ML"; |
27546 | 151 |
use "defs.ML"; |
43795
ca5896a836ba
recovered some runtime sharing from d6b6c74a8bcf, without the global memory bottleneck;
wenzelm
parents:
43794
diff
changeset
|
152 |
use "term_sharing.ML"; |
0 | 153 |
use "pattern.ML"; |
154 |
use "unify.ML"; |
|
1528 | 155 |
use "theory.ML"; |
11511 | 156 |
use "proofterm.ML"; |
0 | 157 |
use "thm.ML"; |
59026
30b8a5825a9c
removed some add-ons from modules that are relevant for the inference kernel;
wenzelm
parents:
58928
diff
changeset
|
158 |
use "more_pattern.ML"; |
30b8a5825a9c
removed some add-ons from modules that are relevant for the inference kernel;
wenzelm
parents:
58928
diff
changeset
|
159 |
use "more_unify.ML"; |
22361 | 160 |
use "more_thm.ML"; |
26279 | 161 |
use "facts.ML"; |
39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents:
39508
diff
changeset
|
162 |
use "global_theory.ML"; |
3986 | 163 |
use "pure_thy.ML"; |
0 | 164 |
use "drule.ML"; |
22233 | 165 |
use "morphism.ML"; |
19898 | 166 |
use "variable.ML"; |
24833 | 167 |
use "conv.ML"; |
32187 | 168 |
use "goal_display.ML"; |
32169 | 169 |
use "tactical.ML"; |
1582 | 170 |
use "search.ML"; |
21708 | 171 |
use "tactic.ML"; |
41228
e1fce873b814
renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
wenzelm
parents:
40748
diff
changeset
|
172 |
use "raw_simplifier.ML"; |
19417 | 173 |
use "conjunction.ML"; |
20225 | 174 |
use "assumption.ML"; |
0 | 175 |
|
31432
9858f32f9569
just one ROOT.ML without any cd or ".." -- simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset
|
176 |
|
9858f32f9569
just one ROOT.ML without any cd or ".." -- simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset
|
177 |
(* Isar -- Intelligible Semi-Automated Reasoning *) |
9858f32f9569
just one ROOT.ML without any cd or ".." -- simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset
|
178 |
|
56303
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
56288
diff
changeset
|
179 |
(*ML support and global execution*) |
49041
9edfd36a0355
more informative error message from failed goal forks (violating old-style TTY protocol!);
wenzelm
parents:
48990
diff
changeset
|
180 |
use "ML/ml_syntax.ML"; |
9edfd36a0355
more informative error message from failed goal forks (violating old-style TTY protocol!);
wenzelm
parents:
48990
diff
changeset
|
181 |
use "ML/ml_env.ML"; |
56303
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
56288
diff
changeset
|
182 |
use "ML/ml_options.ML"; |
62878 | 183 |
use "ML/ml_print_depth.ML"; |
62498 | 184 |
use_no_debug "ML/exn_debugger.ML"; |
185 |
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
|
186 |
use "PIDE/execution.ML"; |
62355 | 187 |
use "ML/ml_compiler.ML"; |
49041
9edfd36a0355
more informative error message from failed goal forks (violating old-style TTY protocol!);
wenzelm
parents:
48990
diff
changeset
|
188 |
|
51551 | 189 |
use "skip_proof.ML"; |
49041
9edfd36a0355
more informative error message from failed goal forks (violating old-style TTY protocol!);
wenzelm
parents:
48990
diff
changeset
|
190 |
use "goal.ML"; |
9edfd36a0355
more informative error message from failed goal forks (violating old-style TTY protocol!);
wenzelm
parents:
48990
diff
changeset
|
191 |
|
31432
9858f32f9569
just one ROOT.ML without any cd or ".." -- simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset
|
192 |
(*proof context*) |
9858f32f9569
just one ROOT.ML without any cd or ".." -- simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset
|
193 |
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
|
194 |
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
|
195 |
use "Isar/auto_bind.ML"; |
42241
dd8029f71e1c
separate module for standard implementation of inner syntax operations;
wenzelm
parents:
42240
diff
changeset
|
196 |
use "type_infer.ML"; |
42240
5a4d30cd47a7
moved Isar/local_syntax.ML to Syntax/local_syntax.ML;
wenzelm
parents:
42012
diff
changeset
|
197 |
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
|
198 |
use "Isar/proof_context.ML"; |
42405
13ecdb3057d8
split Type_Infer into early and late part, after Proof_Context;
wenzelm
parents:
42383
diff
changeset
|
199 |
use "type_infer_context.ML"; |
42243 | 200 |
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
|
201 |
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
|
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*) |
58903 | 204 |
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
|
205 |
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
|
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 |
|
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
|
209 |
(*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
|
210 |
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
|
211 |
use "Thy/thy_header.ML"; |
57905
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
57649
diff
changeset
|
212 |
use "PIDE/command_span.ML"; |
51265 | 213 |
use "Thy/thy_syntax.ML"; |
61454 | 214 |
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
|
215 |
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
|
216 |
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
|
217 |
|
56203
76c72f4d0667
clarified bootstrap process: switch to ML with context and antiquotations earlier;
wenzelm
parents:
56072
diff
changeset
|
218 |
(*ML with context and antiquotations*) |
76c72f4d0667
clarified bootstrap process: switch to ML with context and antiquotations earlier;
wenzelm
parents:
56072
diff
changeset
|
219 |
use "ML/ml_context.ML"; |
56205 | 220 |
use "ML/ml_antiquotation.ML"; |
62817 | 221 |
use "ML/ml_compiler2.ML"; |
56434 | 222 |
|
56288 | 223 |
|
224 |
||
62870 | 225 |
(** bootstrap phase 3: towards theory "Pure" and final ML toplevel setup *) |
56203
76c72f4d0667
clarified bootstrap process: switch to ML with context and antiquotations earlier;
wenzelm
parents:
56072
diff
changeset
|
226 |
|
31432
9858f32f9569
just one ROOT.ML without any cd or ".." -- simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset
|
227 |
(*basic proof engine*) |
58009 | 228 |
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
|
229 |
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
|
230 |
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
|
231 |
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
|
232 |
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
|
233 |
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
|
234 |
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
|
235 |
use "Isar/obtain.ML"; |
60630 | 236 |
use "Isar/subgoal.ML"; |
62848
e4140efe699e
clarified bootstrap -- more uniform use of ML files;
wenzelm
parents:
62847
diff
changeset
|
237 |
use "Isar/calculation.ML"; |
31432
9858f32f9569
just one ROOT.ML without any cd or ".." -- simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset
|
238 |
|
9858f32f9569
just one ROOT.ML without any cd or ".." -- simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset
|
239 |
(*local theories and targets*) |
52140 | 240 |
use "Isar/locale.ML"; |
38307
0028571ade2d
split off structure Generic_Target into separate file
haftmann
parents:
38150
diff
changeset
|
241 |
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
|
242 |
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
|
243 |
use "axclass.ML"; |
38379
67d71449e85b
more convenient split of class modules: class and class_declaration
haftmann
parents:
38350
diff
changeset
|
244 |
use "Isar/class.ML"; |
38350
480b2de9927c
renamed Theory_Target to the more appropriate Named_Target
haftmann
parents:
38343
diff
changeset
|
245 |
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
|
246 |
use "Isar/expression.ML"; |
61669 | 247 |
use "Isar/interpretation.ML"; |
38379
67d71449e85b
more convenient split of class modules: class and class_declaration
haftmann
parents:
38350
diff
changeset
|
248 |
use "Isar/class_declaration.ML"; |
47057 | 249 |
use "Isar/bundle.ML"; |
59901 | 250 |
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
|
251 |
|
9858f32f9569
just one ROOT.ML without any cd or ".." -- simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset
|
252 |
use "simplifier.ML"; |
58660 | 253 |
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
|
254 |
|
9858f32f9569
just one ROOT.ML without any cd or ".." -- simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset
|
255 |
(*executable theory content*) |
9858f32f9569
just one ROOT.ML without any cd or ".." -- simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset
|
256 |
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
|
257 |
|
9858f32f9569
just one ROOT.ML without any cd or ".." -- simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset
|
258 |
(*specifications*) |
36952
338c3f8229e4
renamed structure SpecParse to Parse_Spec, keeping the old name as alias for some time;
wenzelm
parents:
36951
diff
changeset
|
259 |
use "Isar/parse_spec.ML"; |
33374
8099185908a4
Rules that characterize functional/relational specifications.
wenzelm
parents:
32840
diff
changeset
|
260 |
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
|
261 |
use "Isar/specification.ML"; |
35626 | 262 |
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
|
263 |
|
9858f32f9569
just one ROOT.ML without any cd or ".." -- simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset
|
264 |
(*toplevel transactions*) |
9858f32f9569
just one ROOT.ML without any cd or ".." -- simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset
|
265 |
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
|
266 |
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
|
267 |
|
56206 | 268 |
(*proof term operations*) |
269 |
use "Proof/reconstruct.ML"; |
|
270 |
use "Proof/proof_syntax.ML"; |
|
271 |
use "Proof/proof_rewrite_rules.ML"; |
|
272 |
use "Proof/proof_checker.ML"; |
|
273 |
use "Proof/extraction.ML"; |
|
274 |
||
62584 | 275 |
(*Isabelle system*) |
62879
4764473c9b8d
back to static conditional compilation -- simplified bootstrap;
wenzelm
parents:
62878
diff
changeset
|
276 |
use "System/$ISABELLE_WINDOWS_PREFIX/bash.ML"; |
62584 | 277 |
use "System/isabelle_system.ML"; |
278 |
||
62845 | 279 |
|
38271
36187e8443dd
Isar_Document command input via native Isabelle_Process commands, using YXML and XML_Data representation;
wenzelm
parents:
38266
diff
changeset
|
280 |
(*theory documents*) |
31432
9858f32f9569
just one ROOT.ML without any cd or ".." -- simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset
|
281 |
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
|
282 |
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
|
283 |
use "Thy/thy_output.ML"; |
61619 | 284 |
use "Thy/document_antiquotations.ML"; |
49561 | 285 |
use "General/graph_display.ML"; |
43712
3c2c912af2ef
moved Outer_Syntax.load_thy to Thy_Load.load_thy;
wenzelm
parents:
43684
diff
changeset
|
286 |
use "Thy/present.ML"; |
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58903
diff
changeset
|
287 |
use "pure_syn.ML"; |
52510 | 288 |
use "PIDE/command.ML"; |
52865
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
52836
diff
changeset
|
289 |
use "PIDE/query_operation.ML"; |
56208 | 290 |
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
|
291 |
use "Thy/thy_info.ML"; |
59086
94b2690ad494
node-specific keywords, with session base syntax as default;
wenzelm
parents:
59064
diff
changeset
|
292 |
use "PIDE/session.ML"; |
59714
ae322325adbb
tuned protocol -- resolve command positions in ML;
wenzelm
parents:
59470
diff
changeset
|
293 |
use "PIDE/protocol_message.ML"; |
44185 | 294 |
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
|
295 |
|
9858f32f9569
just one ROOT.ML without any cd or ".." -- simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset
|
296 |
(*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
|
297 |
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
|
298 |
|
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 |
(* Isabelle/Isar system *) |
9858f32f9569
just one ROOT.ML without any cd or ".." -- simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset
|
301 |
|
48681
181b91e1d1c1
prefer general Command_Line.tool wrapper (cf. Scala version);
wenzelm
parents:
48646
diff
changeset
|
302 |
use "System/command_line.ML"; |
45029
63144ea111f7
abstract System_Channel in ML (cf. Scala version);
wenzelm
parents:
45026
diff
changeset
|
303 |
use "System/system_channel.ML"; |
52584 | 304 |
use "System/message_channel.ML"; |
38412
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
38379
diff
changeset
|
305 |
use "System/isabelle_process.ML"; |
43748 | 306 |
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
|
307 |
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
|
308 |
|
31432
9858f32f9569
just one ROOT.ML without any cd or ".." -- simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset
|
309 |
|
9858f32f9569
just one ROOT.ML without any cd or ".." -- simplifies ML environment references to bootstrap sources;
wenzelm
parents:
31335
diff
changeset
|
310 |
(* 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
|
311 |
|
62849
caaa2fc4040d
clarified bootstrap -- avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset
|
312 |
use "ML/ml_pp.ML"; |
caaa2fc4040d
clarified bootstrap -- avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset
|
313 |
use "ML/ml_antiquotations.ML"; |
caaa2fc4040d
clarified bootstrap -- avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset
|
314 |
use "ML/ml_thms.ML"; |
62862 | 315 |
use "ML/ml_file.ML"; |
62849
caaa2fc4040d
clarified bootstrap -- avoid 'ML_file' in Pure.thy for uniformity;
wenzelm
parents:
62848
diff
changeset
|
316 |
|
50686 | 317 |
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
|
318 |
use "Tools/named_thms.ML"; |
62848
e4140efe699e
clarified bootstrap -- more uniform use of ML files;
wenzelm
parents:
62847
diff
changeset
|
319 |
use "Tools/print_operation.ML"; |
e4140efe699e
clarified bootstrap -- more uniform use of ML files;
wenzelm
parents:
62847
diff
changeset
|
320 |
use "Tools/bibtex.ML"; |
e4140efe699e
clarified bootstrap -- more uniform use of ML files;
wenzelm
parents:
62847
diff
changeset
|
321 |
use "Tools/rail.ML"; |
e4140efe699e
clarified bootstrap -- more uniform use of ML files;
wenzelm
parents:
62847
diff
changeset
|
322 |
use "Tools/rule_insts.ML"; |
e4140efe699e
clarified bootstrap -- more uniform use of ML files;
wenzelm
parents:
62847
diff
changeset
|
323 |
use "Tools/thm_deps.ML"; |
e4140efe699e
clarified bootstrap -- more uniform use of ML files;
wenzelm
parents:
62847
diff
changeset
|
324 |
use "Tools/thy_deps.ML"; |
e4140efe699e
clarified bootstrap -- more uniform use of ML files;
wenzelm
parents:
62847
diff
changeset
|
325 |
use "Tools/class_deps.ML"; |
e4140efe699e
clarified bootstrap -- more uniform use of ML files;
wenzelm
parents:
62847
diff
changeset
|
326 |
use "Tools/find_theorems.ML"; |
e4140efe699e
clarified bootstrap -- more uniform use of ML files;
wenzelm
parents:
62847
diff
changeset
|
327 |
use "Tools/find_consts.ML"; |
e4140efe699e
clarified bootstrap -- more uniform use of ML files;
wenzelm
parents:
62847
diff
changeset
|
328 |
use "Tools/simplifier_trace.ML"; |
e4140efe699e
clarified bootstrap -- more uniform use of ML files;
wenzelm
parents:
62847
diff
changeset
|
329 |
use_no_debug "Tools/debugger.ML"; |
e4140efe699e
clarified bootstrap -- more uniform use of ML files;
wenzelm
parents:
62847
diff
changeset
|
330 |
use "Tools/named_theorems.ML"; |
e4140efe699e
clarified bootstrap -- more uniform use of ML files;
wenzelm
parents:
62847
diff
changeset
|
331 |
use "Tools/jedit.ML"; |