author | wenzelm |
Thu, 02 Aug 2012 12:36:54 +0200 | |
changeset 48646 | 91281e9472d8 |
parent 48641 | 92b48b8abfe4 |
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 |
||
48638 | 7 |
(* ML toplevel use commands *) |
8 |
||
9 |
fun use name = Toplevel.program (fn () => Thy_Load.use_ml (Path.explode name)); |
|
10 |
||
11 |
fun use_thys name = Toplevel.program (fn () => Thy_Info.use_thys name); |
|
12 |
fun use_thy name = Toplevel.program (fn () => Thy_Info.use_thy name); |
|
13 |
||
14 |
||
37954
a2e73df0b1e0
simplified/clarified register_thy: more precise treatment of new dependencies, remove descendants;
wenzelm
parents:
37949
diff
changeset
|
15 |
(* the Pure theory *) |
24053
af1dd276fae0
added ML toplevel use commands: Toplevel.program;
wenzelm
parents:
23828
diff
changeset
|
16 |
|
48641
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset
|
17 |
val _ = |
48646
91281e9472d8
more official command specifications, including source position;
wenzelm
parents:
48641
diff
changeset
|
18 |
Outer_Syntax.command |
91281e9472d8
more official command specifications, including source position;
wenzelm
parents:
48641
diff
changeset
|
19 |
(("theory", Keyword.tag_theory Keyword.thy_begin), Position.none) "begin theory context" |
48641
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset
|
20 |
(Thy_Header.args >> (fn header => |
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset
|
21 |
Toplevel.print o |
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset
|
22 |
Toplevel.init_theory |
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset
|
23 |
(fn () => Thy_Info.toplevel_begin_theory (Thy_Load.get_master_path ()) header))); |
92b48b8abfe4
more standard bootstrapping of Pure outer syntax;
wenzelm
parents:
48638
diff
changeset
|
24 |
|
48638 | 25 |
Unsynchronized.setmp Multithreading.max_threads 1 |
26 |
use_thy "Pure"; |
|
27 |
Context.set_thread_data NONE; |
|
37954
a2e73df0b1e0
simplified/clarified register_thy: more precise treatment of new dependencies, remove descendants;
wenzelm
parents:
37949
diff
changeset
|
28 |
|
48638 | 29 |
structure Pure = struct val thy = Thy_Info.get_theory "Pure" end; |
23828 | 30 |
|
24053
af1dd276fae0
added ML toplevel use commands: Toplevel.program;
wenzelm
parents:
23828
diff
changeset
|
31 |
|
af1dd276fae0
added ML toplevel use commands: Toplevel.program;
wenzelm
parents:
23828
diff
changeset
|
32 |
(* ML toplevel pretty printing *) |
af1dd276fae0
added ML toplevel use commands: Toplevel.program;
wenzelm
parents:
23828
diff
changeset
|
33 |
|
37529 | 34 |
toplevel_pp ["Pretty", "T"] "(fn _: Pretty.T => Pretty.str \"<pretty>\")"; |
30625
d53d1a16d5ee
replaced install_pp/make_pp by more general toplevel_pp based on use_text;
wenzelm
parents:
30621
diff
changeset
|
35 |
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
|
36 |
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
|
37 |
toplevel_pp ["Position", "T"] "Pretty.position"; |
42381
309ec68442c6
added Binding.print convenience, which includes quote already;
wenzelm
parents:
42360
diff
changeset
|
38 |
toplevel_pp ["Binding", "binding"] "Pretty.str o Binding.print"; |
33389 | 39 |
toplevel_pp ["Thm", "thm"] "Proof_Display.pp_thm"; |
40 |
toplevel_pp ["Thm", "cterm"] "Proof_Display.pp_cterm"; |
|
41 |
toplevel_pp ["Thm", "ctyp"] "Proof_Display.pp_ctyp"; |
|
42 |
toplevel_pp ["typ"] "Proof_Display.pp_typ Pure.thy"; |
|
30625
d53d1a16d5ee
replaced install_pp/make_pp by more general toplevel_pp based on use_text;
wenzelm
parents:
30621
diff
changeset
|
43 |
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
|
44 |
toplevel_pp ["Context", "theory_ref"] "Context.pretty_thy o Theory.deref"; |
33389 | 45 |
toplevel_pp ["Context", "Proof", "context"] "Proof_Display.pp_context"; |
42261 | 46 |
toplevel_pp ["Ast", "ast"] "Ast.pretty_ast"; |
43593 | 47 |
toplevel_pp ["Path", "T"] "Path.pretty"; |
41954 | 48 |
toplevel_pp ["SHA1", "digest"] "Pretty.str o quote o SHA1.rep"; |
37858 | 49 |
toplevel_pp ["Proof", "state"] "(fn _: Proof.state => Pretty.str \"<Proof.state>\")"; |
50 |
toplevel_pp ["Toplevel", "state"] "Toplevel.pretty_abstract"; |
|
24053
af1dd276fae0
added ML toplevel use commands: Toplevel.program;
wenzelm
parents:
23828
diff
changeset
|
51 |
|
47980
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
47979
diff
changeset
|
52 |
if ML_System.is_polyml then use "ML/install_pp_polyml.ML" else (); |
33917
186262d7cabf
workaround for strange compiler crash of Poly/ML 5.0 and 5.1 at this point http://isabelle.in.tum.de/repos/isabelle/file/a2fc533175ff/src/HOL/Tools/Nitpick/nitpick_nut.ML#l997
wenzelm
parents:
33538
diff
changeset
|
53 |
|
24053
af1dd276fae0
added ML toplevel use commands: Toplevel.program;
wenzelm
parents:
23828
diff
changeset
|
54 |
|
af1dd276fae0
added ML toplevel use commands: Toplevel.program;
wenzelm
parents:
23828
diff
changeset
|
55 |
(* misc *) |
af1dd276fae0
added ML toplevel use commands: Toplevel.program;
wenzelm
parents:
23828
diff
changeset
|
56 |
|
23828 | 57 |
val cd = File.cd o Path.explode; |
58 |
||
25223 | 59 |
Proofterm.proofs := 0; |
42360 | 60 |