author | wenzelm |
Wed, 12 Nov 1997 16:23:11 +0100 | |
changeset 4216 | 419113535e48 |
parent 4214 | 523f6bea9fd7 |
child 4339 | b75312b2676d |
permissions | -rw-r--r-- |
390 | 1 |
(* Title: Pure/Thy/ROOT.ML |
0 | 2 |
ID: $Id$ |
390 | 3 |
Author: Sonia Mahjoub and Tobias Nipkow and |
4 |
Markus Wenzel and Carsten Clasohm, TU Muenchen |
|
0 | 5 |
|
390 | 6 |
This file builds the theory parser and autoloading system. |
0 | 7 |
*) |
8 |
||
4115 | 9 |
use "path.ML"; |
4214 | 10 |
use "file.ML"; |
11 |
use "use.ML"; |
|
4115 | 12 |
|
390 | 13 |
use "thy_scan.ML"; |
14 |
use "thy_parse.ML"; |
|
413 | 15 |
use "thy_syn.ML"; |
3619 | 16 |
|
3600
5366dde08dba
Added some additional "use" commands for new files
berghofe
parents:
3576
diff
changeset
|
17 |
use "thy_info.ML"; |
5366dde08dba
Added some additional "use" commands for new files
berghofe
parents:
3576
diff
changeset
|
18 |
use "browser_info.ML"; |
1132
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
1078
diff
changeset
|
19 |
use "thm_database.ML"; |
413 | 20 |
use "thy_read.ML"; |
0 | 21 |
|
4214 | 22 |
open ThmDatabase ThyRead ThyInfo BrowserInfo; |
1078 | 23 |
|
2809 | 24 |
|
4055 | 25 |
|
26 |
(* FIXME tmp, move *) |
|
27 |
||
28 |
structure Session = |
|
29 |
struct |
|
30 |
||
31 |
local |
|
32 |
val current_session = ref ([]: string list); |
|
33 |
in |
|
34 |
fun get_session () = ! current_session; |
|
35 |
fun add_session s = |
|
36 |
(current_session := ! current_session @ [s]; |
|
37 |
writeln ("This is the " ^ quote (space_implode "/" (get_session ())) ^ " session.")); |
|
38 |
end; |
|
39 |
||
40 |
end; |
|
2809 | 41 |
|
4055 | 42 |
open Session |
43 |
||
44 |
||
45 |
structure Context = |
|
46 |
struct |
|
47 |
||
48 |
local |
|
49 |
val current_thy = ref ProtoPure.thy; |
|
50 |
in |
|
51 |
fun context thy = current_thy := thy; |
|
52 |
fun get_context () = ! current_thy; |
|
53 |
end; |
|
54 |
||
55 |
end; |
|
56 |
||
57 |
open Context; |