src/Pure/pure_setup.ML
author wenzelm
Thu Aug 30 15:04:42 2007 +0200 (2007-08-30 ago)
changeset 24484 013b98b57b86
parent 24242 e52ef498c0ba
child 24960 39d1dd215d73
permissions -rw-r--r--
maintain mode in context (get/set/restore_mode);
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@23828
    19
use_thy "Pure";
wenzelm@23828
    20
structure Pure = struct val thy = theory "Pure" end;
wenzelm@23828
    21
wenzelm@23828
    22
Context.add_setup
wenzelm@24242
    23
 (Sign.del_modesyntax_i Syntax.default_mode PureThy.appl_syntax #>
wenzelm@24242
    24
  Sign.add_syntax_i PureThy.applC_syntax);
wenzelm@23828
    25
use_thy "CPure";
wenzelm@23828
    26
structure CPure = struct val thy = theory "CPure" end;
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@23828
    47
proofs := 0;