src/Pure/pure_setup.ML
author wenzelm
Sun Mar 01 23:36:12 2009 +0100 (2009-03-01)
changeset 30190 479806475f3c
parent 29618 8161c8e3fa10
child 30218 cdd82ba2b4fd
permissions -rw-r--r--
use long names for old-style fold combinators;
wenzelm@23828
     1
(*  Title:      Pure/pure_setup.ML
wenzelm@23828
     2
    Author:     Makarius
wenzelm@23828
     3
wenzelm@24053
     4
Pure theory and ML toplevel setup.
wenzelm@23828
     5
*)
wenzelm@23828
     6
wenzelm@24053
     7
(* ML toplevel use commands *)
wenzelm@24053
     8
wenzelm@24053
     9
fun use name          = Toplevel.program (fn () => ThyInfo.use name);
wenzelm@24053
    10
fun use_thys name     = Toplevel.program (fn () => ThyInfo.use_thys name);
wenzelm@24053
    11
fun use_thy name      = Toplevel.program (fn () => ThyInfo.use_thy name);
wenzelm@24174
    12
fun time_use name     = Toplevel.program (fn () => ThyInfo.time_use name);
wenzelm@24053
    13
fun time_use_thy name = Toplevel.program (fn () => ThyInfo.time_use_thy name);
wenzelm@24053
    14
wenzelm@24053
    15
wenzelm@24053
    16
(* the Pure theories *)
wenzelm@24053
    17
wenzelm@26608
    18
val theory = ThyInfo.get_theory;
wenzelm@26608
    19
wenzelm@26463
    20
Context.>> (Context.map_theory
wenzelm@26463
    21
 (OuterSyntax.process_file (Path.explode "Pure.thy") #>
wenzelm@26463
    22
  Theory.end_theory));
wenzelm@26427
    23
structure Pure = struct val thy = ML_Context.the_global_context () end;
wenzelm@26427
    24
Context.set_thread_data NONE;
wenzelm@26427
    25
ThyInfo.register_theory Pure.thy;
wenzelm@23828
    26
wenzelm@24053
    27
wenzelm@24053
    28
(* ML toplevel pretty printing *)
wenzelm@24053
    29
wenzelm@29123
    30
install_pp (make_pp ["Task_Queue", "task"] (Pretty.pprint o Pretty.str o Task_Queue.str_of_task));
wenzelm@29123
    31
install_pp (make_pp ["Task_Queue", "group"] (Pretty.pprint o Pretty.str o Task_Queue.str_of_group));
wenzelm@27776
    32
install_pp (make_pp ["Position", "T"] (Pretty.pprint o Pretty.enum "," "{" "}" o
wenzelm@27776
    33
  map (fn (x, y) => Pretty.str (x ^ "=" ^ y)) o Position.properties_of));
wenzelm@24053
    34
install_pp (make_pp ["Thm", "thm"] ProofDisplay.pprint_thm);
wenzelm@24053
    35
install_pp (make_pp ["Thm", "cterm"] ProofDisplay.pprint_cterm);
haftmann@29618
    36
install_pp (make_pp ["Binding", "binding"] (Pretty.pprint o Pretty.str o Binding.display));
wenzelm@24053
    37
install_pp (make_pp ["Thm", "ctyp"] ProofDisplay.pprint_ctyp);
wenzelm@24053
    38
install_pp (make_pp ["Context", "theory"] Context.pprint_thy);
wenzelm@27341
    39
install_pp (make_pp ["Context", "theory_ref"] Context.pprint_thy_ref);
wenzelm@24053
    40
install_pp (make_pp ["Context", "proof"] ProofDisplay.pprint_context);
wenzelm@24053
    41
install_pp (make_pp ["Syntax", "ast"] Syntax.pprint_ast);
wenzelm@24053
    42
install_pp (make_pp ["typ"] (ProofDisplay.pprint_typ Pure.thy));
wenzelm@24053
    43
install_pp (make_pp ["Path", "T"] (Pretty.pprint o Pretty.str o quote o Path.implode));
wenzelm@24053
    44
install_pp (make_pp ["File", "ident"] (Pretty.pprint o Pretty.str o quote o File.rep_ident));
wenzelm@24053
    45
wenzelm@28557
    46
if String.isPrefix "polyml" ml_system then use "ML-Systems/install_pp_polyml.ML"
wenzelm@28557
    47
else ();
wenzelm@28557
    48
wenzelm@24053
    49
wenzelm@24053
    50
(* misc *)
wenzelm@24053
    51
wenzelm@23828
    52
val cd = File.cd o Path.explode;
wenzelm@23828
    53
ml_prompts "ML> " "ML# ";
wenzelm@23828
    54
wenzelm@25223
    55
Proofterm.proofs := 0;