src/Pure/pure_setup.ML
author wenzelm
Wed Mar 26 22:40:03 2008 +0100 (2008-03-26)
changeset 26413 003dd6155870
parent 25223 7463251e7273
child 26427 f33d1b522316
permissions -rw-r--r--
added thread data (formerly global ref in ML/ml_context.ML);
renamed ML_Context.>> to Context.>> (again);
     1 (*  Title:      Pure/pure_setup.ML
     2     ID:         $Id$
     3     Author:     Makarius
     4 
     5 Pure theory and ML toplevel setup.
     6 *)
     7 
     8 (* ML toplevel use commands *)
     9 
    10 fun use name          = Toplevel.program (fn () => ThyInfo.use name);
    11 fun use_thys name     = Toplevel.program (fn () => ThyInfo.use_thys name);
    12 fun use_thy name      = Toplevel.program (fn () => ThyInfo.use_thy name);
    13 fun time_use name     = Toplevel.program (fn () => ThyInfo.time_use name);
    14 fun time_use_thy name = Toplevel.program (fn () => ThyInfo.time_use_thy name);
    15 
    16 
    17 (* the Pure theories *)
    18 
    19 use_thy "Pure";
    20 structure Pure = struct val thy = theory "Pure" end;
    21 
    22 Context.add_setup
    23  (Sign.del_modesyntax_i Syntax.mode_default PureThy.appl_syntax #>
    24   Sign.add_syntax_i PureThy.applC_syntax);
    25 use_thy "CPure";
    26 structure CPure = struct val thy = theory "CPure" end;
    27 
    28 
    29 (* ML toplevel pretty printing *)
    30 
    31 install_pp (make_pp ["Thm", "thm"] ProofDisplay.pprint_thm);
    32 install_pp (make_pp ["Thm", "cterm"] ProofDisplay.pprint_cterm);
    33 install_pp (make_pp ["Thm", "ctyp"] ProofDisplay.pprint_ctyp);
    34 install_pp (make_pp ["Context", "theory"] Context.pprint_thy);
    35 install_pp (make_pp ["Context", "proof"] ProofDisplay.pprint_context);
    36 install_pp (make_pp ["Syntax", "ast"] Syntax.pprint_ast);
    37 install_pp (make_pp ["typ"] (ProofDisplay.pprint_typ Pure.thy));
    38 install_pp (make_pp ["Path", "T"] (Pretty.pprint o Pretty.str o quote o Path.implode));
    39 install_pp (make_pp ["File", "ident"] (Pretty.pprint o Pretty.str o quote o File.rep_ident));
    40 
    41 
    42 (* misc *)
    43 
    44 val cd = File.cd o Path.explode;
    45 ml_prompts "ML> " "ML# ";
    46 
    47 Proofterm.proofs := 0;