author | wenzelm |
Sat, 17 Oct 2009 17:18:59 +0200 | |
changeset 32971 | 55ba9b6648ef |
parent 31646 | ef30cd0e41e5 |
child 33032 | a707a1f37d29 |
permissions | -rw-r--r-- |
23828 | 1 |
(* Title: Pure/pure_setup.ML |
2 |
Author: Makarius |
|
3 |
||
24053
af1dd276fae0
added ML toplevel use commands: Toplevel.program;
wenzelm
parents:
23828
diff
changeset
|
4 |
Pure theory and ML toplevel setup. |
23828 | 5 |
*) |
6 |
||
24053
af1dd276fae0
added ML toplevel use commands: Toplevel.program;
wenzelm
parents:
23828
diff
changeset
|
7 |
(* the Pure theories *) |
af1dd276fae0
added ML toplevel use commands: Toplevel.program;
wenzelm
parents:
23828
diff
changeset
|
8 |
|
26608 | 9 |
val theory = ThyInfo.get_theory; |
10 |
||
26463 | 11 |
Context.>> (Context.map_theory |
12 |
(OuterSyntax.process_file (Path.explode "Pure.thy") #> |
|
13 |
Theory.end_theory)); |
|
26427 | 14 |
structure Pure = struct val thy = ML_Context.the_global_context () end; |
15 |
Context.set_thread_data NONE; |
|
16 |
ThyInfo.register_theory Pure.thy; |
|
23828 | 17 |
|
24053
af1dd276fae0
added ML toplevel use commands: Toplevel.program;
wenzelm
parents:
23828
diff
changeset
|
18 |
|
af1dd276fae0
added ML toplevel use commands: Toplevel.program;
wenzelm
parents:
23828
diff
changeset
|
19 |
(* ML toplevel pretty printing *) |
af1dd276fae0
added ML toplevel use commands: Toplevel.program;
wenzelm
parents:
23828
diff
changeset
|
20 |
|
30625
d53d1a16d5ee
replaced install_pp/make_pp by more general toplevel_pp based on use_text;
wenzelm
parents:
30621
diff
changeset
|
21 |
toplevel_pp ["Task_Queue", "task"] "Pretty.str o Task_Queue.str_of_task"; |
d53d1a16d5ee
replaced install_pp/make_pp by more general toplevel_pp based on use_text;
wenzelm
parents:
30621
diff
changeset
|
22 |
toplevel_pp ["Task_Queue", "group"] "Pretty.str o Task_Queue.str_of_group"; |
d53d1a16d5ee
replaced install_pp/make_pp by more general toplevel_pp based on use_text;
wenzelm
parents:
30621
diff
changeset
|
23 |
toplevel_pp ["Position", "T"] "Pretty.position"; |
d53d1a16d5ee
replaced install_pp/make_pp by more general toplevel_pp based on use_text;
wenzelm
parents:
30621
diff
changeset
|
24 |
toplevel_pp ["Binding", "binding"] "Pretty.str o quote o Binding.str_of"; |
d53d1a16d5ee
replaced install_pp/make_pp by more general toplevel_pp based on use_text;
wenzelm
parents:
30621
diff
changeset
|
25 |
toplevel_pp ["Thm", "thm"] "ProofDisplay.pp_thm"; |
d53d1a16d5ee
replaced install_pp/make_pp by more general toplevel_pp based on use_text;
wenzelm
parents:
30621
diff
changeset
|
26 |
toplevel_pp ["Thm", "cterm"] "ProofDisplay.pp_cterm"; |
d53d1a16d5ee
replaced install_pp/make_pp by more general toplevel_pp based on use_text;
wenzelm
parents:
30621
diff
changeset
|
27 |
toplevel_pp ["Thm", "ctyp"] "ProofDisplay.pp_ctyp"; |
d53d1a16d5ee
replaced install_pp/make_pp by more general toplevel_pp based on use_text;
wenzelm
parents:
30621
diff
changeset
|
28 |
toplevel_pp ["typ"] "ProofDisplay.pp_typ Pure.thy"; |
d53d1a16d5ee
replaced install_pp/make_pp by more general toplevel_pp based on use_text;
wenzelm
parents:
30621
diff
changeset
|
29 |
toplevel_pp ["Context", "theory"] "Context.pretty_thy"; |
d53d1a16d5ee
replaced install_pp/make_pp by more general toplevel_pp based on use_text;
wenzelm
parents:
30621
diff
changeset
|
30 |
toplevel_pp ["Context", "theory_ref"] "Context.pretty_thy o Theory.deref"; |
d53d1a16d5ee
replaced install_pp/make_pp by more general toplevel_pp based on use_text;
wenzelm
parents:
30621
diff
changeset
|
31 |
toplevel_pp ["Context", "proof"] "ProofDisplay.pp_context"; |
d53d1a16d5ee
replaced install_pp/make_pp by more general toplevel_pp based on use_text;
wenzelm
parents:
30621
diff
changeset
|
32 |
toplevel_pp ["Syntax", "ast"] "Syntax.pretty_ast"; |
d53d1a16d5ee
replaced install_pp/make_pp by more general toplevel_pp based on use_text;
wenzelm
parents:
30621
diff
changeset
|
33 |
toplevel_pp ["Path", "T"] "Pretty.str o quote o Path.implode"; |
d53d1a16d5ee
replaced install_pp/make_pp by more general toplevel_pp based on use_text;
wenzelm
parents:
30621
diff
changeset
|
34 |
toplevel_pp ["File", "ident"] "Pretty.str o quote o File.rep_ident"; |
24053
af1dd276fae0
added ML toplevel use commands: Toplevel.program;
wenzelm
parents:
23828
diff
changeset
|
35 |
|
31433 | 36 |
if ml_system = "polyml-experimental" |
37 |
then use "ML-Systems/install_pp_polyml-5.3.ML" |
|
30625
d53d1a16d5ee
replaced install_pp/make_pp by more general toplevel_pp based on use_text;
wenzelm
parents:
30621
diff
changeset
|
38 |
else if String.isPrefix "polyml" ml_system |
d53d1a16d5ee
replaced install_pp/make_pp by more general toplevel_pp based on use_text;
wenzelm
parents:
30621
diff
changeset
|
39 |
then use "ML-Systems/install_pp_polyml.ML" |
28557
6a661aeff564
extra Poly/ML toplevel pretty printing in ML-Systems/install_pp_polyml.ML;
wenzelm
parents:
28414
diff
changeset
|
40 |
else (); |
6a661aeff564
extra Poly/ML toplevel pretty printing in ML-Systems/install_pp_polyml.ML;
wenzelm
parents:
28414
diff
changeset
|
41 |
|
24053
af1dd276fae0
added ML toplevel use commands: Toplevel.program;
wenzelm
parents:
23828
diff
changeset
|
42 |
|
31646 | 43 |
(* ML toplevel use commands *) |
44 |
||
45 |
fun use name = Toplevel.program (fn () => ThyInfo.use name); |
|
46 |
fun use_thys name = Toplevel.program (fn () => ThyInfo.use_thys name); |
|
47 |
fun use_thy name = Toplevel.program (fn () => ThyInfo.use_thy name); |
|
48 |
fun time_use name = Toplevel.program (fn () => ThyInfo.time_use name); |
|
49 |
fun time_use_thy name = Toplevel.program (fn () => ThyInfo.time_use_thy name); |
|
50 |
||
51 |
||
24053
af1dd276fae0
added ML toplevel use commands: Toplevel.program;
wenzelm
parents:
23828
diff
changeset
|
52 |
(* misc *) |
af1dd276fae0
added ML toplevel use commands: Toplevel.program;
wenzelm
parents:
23828
diff
changeset
|
53 |
|
23828 | 54 |
val cd = File.cd o Path.explode; |
55 |
||
25223 | 56 |
Proofterm.proofs := 0; |