src/Pure/pure_setup.ML
author wenzelm
Tue, 20 Jul 2010 20:56:28 +0200
changeset 37858 e1ef6b441fe7
parent 37535 75de61a479e3
child 37860 aa3b3d00698b
permissions -rw-r--r--
toplevel pp for Proof.state and Toplevel.state;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
23828
a8a3962f8eeb Pure theory setup.
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/pure_setup.ML
a8a3962f8eeb Pure theory setup.
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
a8a3962f8eeb Pure theory setup.
wenzelm
parents:
diff changeset
     3
24053
af1dd276fae0 added ML toplevel use commands: Toplevel.program;
wenzelm
parents: 23828
diff changeset
     4
Pure theory and ML toplevel setup.
23828
a8a3962f8eeb Pure theory setup.
wenzelm
parents:
diff changeset
     5
*)
a8a3962f8eeb Pure theory setup.
wenzelm
parents:
diff changeset
     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
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 36953
diff changeset
     9
val theory = Thy_Info.get_theory;
26608
ff838a61dad6 val theory = ThyInfo.get_theory;
wenzelm
parents: 26463
diff changeset
    10
26463
9283b4185fdf Context.>> : operate on Context.generic;
wenzelm
parents: 26435
diff changeset
    11
Context.>> (Context.map_theory
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 33917
diff changeset
    12
 (Outer_Syntax.process_file (Path.explode "Pure.thy") #>
26463
9283b4185fdf Context.>> : operate on Context.generic;
wenzelm
parents: 26435
diff changeset
    13
  Theory.end_theory));
26427
f33d1b522316 implicit setup of emerging theory Pure;
wenzelm
parents: 25223
diff changeset
    14
structure Pure = struct val thy = ML_Context.the_global_context () end;
f33d1b522316 implicit setup of emerging theory Pure;
wenzelm
parents: 25223
diff changeset
    15
Context.set_thread_data NONE;
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 36953
diff changeset
    16
Thy_Info.register_theory Pure.thy;
23828
a8a3962f8eeb Pure theory setup.
wenzelm
parents:
diff changeset
    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
37535
75de61a479e3 ML pretty printing of type string according to (quasi-abstract) YXML markup and symbols (including UTF8);
wenzelm
parents: 37529
diff changeset
    21
toplevel_pp ["String", "string"] "ML_Syntax.pretty_string";
37529
a23e8aa853eb treat Pretty.T as strictly abstract type;
wenzelm
parents: 37216
diff changeset
    22
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
    23
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
    24
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
    25
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
    26
toplevel_pp ["Binding", "binding"] "Pretty.str o quote o Binding.str_of";
33389
bb3a5fa94a91 modernized structure Proof_Display;
wenzelm
parents: 33032
diff changeset
    27
toplevel_pp ["Thm", "thm"] "Proof_Display.pp_thm";
bb3a5fa94a91 modernized structure Proof_Display;
wenzelm
parents: 33032
diff changeset
    28
toplevel_pp ["Thm", "cterm"] "Proof_Display.pp_cterm";
bb3a5fa94a91 modernized structure Proof_Display;
wenzelm
parents: 33032
diff changeset
    29
toplevel_pp ["Thm", "ctyp"] "Proof_Display.pp_ctyp";
bb3a5fa94a91 modernized structure Proof_Display;
wenzelm
parents: 33032
diff changeset
    30
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
    31
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
    32
toplevel_pp ["Context", "theory_ref"] "Context.pretty_thy o Theory.deref";
33389
bb3a5fa94a91 modernized structure Proof_Display;
wenzelm
parents: 33032
diff changeset
    33
toplevel_pp ["Context", "Proof", "context"] "Proof_Display.pp_context";
30625
d53d1a16d5ee replaced install_pp/make_pp by more general toplevel_pp based on use_text;
wenzelm
parents: 30621
diff changeset
    34
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
    35
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
    36
toplevel_pp ["File", "ident"] "Pretty.str o quote o File.rep_ident";
37858
e1ef6b441fe7 toplevel pp for Proof.state and Toplevel.state;
wenzelm
parents: 37535
diff changeset
    37
toplevel_pp ["Proof", "state"] "(fn _: Proof.state => Pretty.str \"<Proof.state>\")";
e1ef6b441fe7 toplevel pp for Proof.state and Toplevel.state;
wenzelm
parents: 37535
diff changeset
    38
toplevel_pp ["Toplevel", "state"] "Toplevel.pretty_abstract";
24053
af1dd276fae0 added ML toplevel use commands: Toplevel.program;
wenzelm
parents: 23828
diff changeset
    39
33538
edf497b5b5d2 setup for official Poly/ML 5.3.0, which is now the default;
wenzelm
parents: 33389
diff changeset
    40
if ml_system = "polyml-5.3.0"
31433
12f5f6af3d2d less experimental polyml-5.3;
wenzelm
parents: 30625
diff changeset
    41
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
    42
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
    43
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
    44
else ();
6a661aeff564 extra Poly/ML toplevel pretty printing in ML-Systems/install_pp_polyml.ML;
wenzelm
parents: 28414
diff changeset
    45
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
    46
if ml_system = "polyml-5.0" orelse ml_system = "polyml-5.1" then
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
    47
  Secure.use_text ML_Parse.global_context (0, "") false
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
    48
    "PolyML.Compiler.maxInlineSize := 20"
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
    49
else ();
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
    50
24053
af1dd276fae0 added ML toplevel use commands: Toplevel.program;
wenzelm
parents: 23828
diff changeset
    51
31646
ef30cd0e41e5 override toplevel "use" functions last;
wenzelm
parents: 31433
diff changeset
    52
(* ML toplevel use commands *)
ef30cd0e41e5 override toplevel "use" functions last;
wenzelm
parents: 31433
diff changeset
    53
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 36953
diff changeset
    54
fun use name = Toplevel.program (fn () => Thy_Info.use name);
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 36953
diff changeset
    55
fun use_thys name = Toplevel.program (fn () => Thy_Info.use_thys name);
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 36953
diff changeset
    56
fun use_thy name = Toplevel.program (fn () => Thy_Info.use_thy name);
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 36953
diff changeset
    57
fun time_use name = Toplevel.program (fn () => Thy_Info.time_use name);
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 36953
diff changeset
    58
fun time_use_thy name = Toplevel.program (fn () => Thy_Info.time_use_thy name);
31646
ef30cd0e41e5 override toplevel "use" functions last;
wenzelm
parents: 31433
diff changeset
    59
ef30cd0e41e5 override toplevel "use" functions last;
wenzelm
parents: 31433
diff changeset
    60
24053
af1dd276fae0 added ML toplevel use commands: Toplevel.program;
wenzelm
parents: 23828
diff changeset
    61
(* misc *)
af1dd276fae0 added ML toplevel use commands: Toplevel.program;
wenzelm
parents: 23828
diff changeset
    62
23828
a8a3962f8eeb Pure theory setup.
wenzelm
parents:
diff changeset
    63
val cd = File.cd o Path.explode;
a8a3962f8eeb Pure theory setup.
wenzelm
parents:
diff changeset
    64
25223
7463251e7273 qualified Proofterm.proofs;
wenzelm
parents: 24960
diff changeset
    65
Proofterm.proofs := 0;