# HG changeset patch
# User wenzelm
# Date 1185717602 -7200
# Node ID af1dd276fae085c5af5fae5c9ed05627ad9b740e
# Parent  90dd4df2c7c39b81ab081e0ca06db1dee55f1637
added ML toplevel use commands: Toplevel.program;
added install_pp stuff;

diff -r 90dd4df2c7c3 -r af1dd276fae0 src/Pure/pure_setup.ML
--- a/src/Pure/pure_setup.ML	Sun Jul 29 16:00:00 2007 +0200
+++ b/src/Pure/pure_setup.ML	Sun Jul 29 16:00:02 2007 +0200
@@ -2,9 +2,21 @@
     ID:         $Id$
     Author:     Makarius
 
-Pure theory setup.
+Pure theory and ML toplevel setup.
 *)
 
+(* ML toplevel use commands *)
+
+fun use name          = Toplevel.program (fn () => ThyInfo.use name);
+fun time_use name     = Toplevel.program (fn () => ThyInfo.time_use name);
+fun use_thys name     = Toplevel.program (fn () => ThyInfo.use_thys name);
+fun use_thy name      = Toplevel.program (fn () => ThyInfo.use_thy name);
+fun time_use_thy name = Toplevel.program (fn () => ThyInfo.time_use_thy name);
+fun update_thy name   = Toplevel.program (fn () => ThyInfo.update_thy name);
+
+
+(* the Pure theories *)
+
 use_thy "Pure";
 structure Pure = struct val thy = theory "Pure" end;
 
@@ -14,8 +26,22 @@
 use_thy "CPure";
 structure CPure = struct val thy = theory "CPure" end;
 
-use "install_pp.ML";
-val use = ThyInfo.use;
+
+(* ML toplevel pretty printing *)
+
+install_pp (make_pp ["Thm", "thm"] ProofDisplay.pprint_thm);
+install_pp (make_pp ["Thm", "cterm"] ProofDisplay.pprint_cterm);
+install_pp (make_pp ["Thm", "ctyp"] ProofDisplay.pprint_ctyp);
+install_pp (make_pp ["Context", "theory"] Context.pprint_thy);
+install_pp (make_pp ["Context", "proof"] ProofDisplay.pprint_context);
+install_pp (make_pp ["Syntax", "ast"] Syntax.pprint_ast);
+install_pp (make_pp ["typ"] (ProofDisplay.pprint_typ Pure.thy));
+install_pp (make_pp ["Path", "T"] (Pretty.pprint o Pretty.str o quote o Path.implode));
+install_pp (make_pp ["File", "ident"] (Pretty.pprint o Pretty.str o quote o File.rep_ident));
+
+
+(* misc *)
+
 val cd = File.cd o Path.explode;
 ml_prompts "ML> " "ML# ";