src/Pure/pure_setup.ML
author wenzelm
Fri Jun 13 21:04:42 2008 +0200 (2008-06-13)
changeset 27195 bbf4cbc69243
parent 26957 e3f04fdd994d
child 27341 97e2ccba3b64
permissions -rw-r--r--
map_const: soft version, no failure here;
wenzelm@23828
     1
(*  Title:      Pure/pure_setup.ML
wenzelm@23828
     2
    ID:         $Id$
wenzelm@23828
     3
    Author:     Makarius
wenzelm@23828
     4
wenzelm@24053
     5
Pure theory and ML toplevel setup.
wenzelm@23828
     6
*)
wenzelm@23828
     7
wenzelm@24053
     8
(* ML toplevel use commands *)
wenzelm@24053
     9
wenzelm@24053
    10
fun use name          = Toplevel.program (fn () => ThyInfo.use name);
wenzelm@24053
    11
fun use_thys name     = Toplevel.program (fn () => ThyInfo.use_thys name);
wenzelm@24053
    12
fun use_thy name      = Toplevel.program (fn () => ThyInfo.use_thy name);
wenzelm@24174
    13
fun time_use name     = Toplevel.program (fn () => ThyInfo.time_use name);
wenzelm@24053
    14
fun time_use_thy name = Toplevel.program (fn () => ThyInfo.time_use_thy name);
wenzelm@24053
    15
wenzelm@24053
    16
wenzelm@24053
    17
(* the Pure theories *)
wenzelm@24053
    18
wenzelm@26608
    19
val theory = ThyInfo.get_theory;
wenzelm@26608
    20
wenzelm@26463
    21
Context.>> (Context.map_theory
wenzelm@26463
    22
 (OuterSyntax.process_file (Path.explode "Pure.thy") #>
wenzelm@26463
    23
  Theory.end_theory));
wenzelm@26427
    24
structure Pure = struct val thy = ML_Context.the_global_context () end;
wenzelm@26427
    25
Context.set_thread_data NONE;
wenzelm@26427
    26
ThyInfo.register_theory Pure.thy;
wenzelm@23828
    27
wenzelm@24053
    28
wenzelm@24053
    29
(* ML toplevel pretty printing *)
wenzelm@24053
    30
wenzelm@24053
    31
install_pp (make_pp ["Thm", "thm"] ProofDisplay.pprint_thm);
wenzelm@24053
    32
install_pp (make_pp ["Thm", "cterm"] ProofDisplay.pprint_cterm);
wenzelm@24053
    33
install_pp (make_pp ["Thm", "ctyp"] ProofDisplay.pprint_ctyp);
wenzelm@24053
    34
install_pp (make_pp ["Context", "theory"] Context.pprint_thy);
wenzelm@24053
    35
install_pp (make_pp ["Context", "proof"] ProofDisplay.pprint_context);
wenzelm@24053
    36
install_pp (make_pp ["Syntax", "ast"] Syntax.pprint_ast);
wenzelm@24053
    37
install_pp (make_pp ["typ"] (ProofDisplay.pprint_typ Pure.thy));
wenzelm@24053
    38
install_pp (make_pp ["Path", "T"] (Pretty.pprint o Pretty.str o quote o Path.implode));
wenzelm@24053
    39
install_pp (make_pp ["File", "ident"] (Pretty.pprint o Pretty.str o quote o File.rep_ident));
wenzelm@24053
    40
wenzelm@24053
    41
wenzelm@24053
    42
(* misc *)
wenzelm@24053
    43
wenzelm@23828
    44
val cd = File.cd o Path.explode;
wenzelm@23828
    45
ml_prompts "ML> " "ML# ";
wenzelm@23828
    46
wenzelm@25223
    47
Proofterm.proofs := 0;