author  paulson 
Fri, 05 Oct 2007 09:59:03 +0200  
changeset 24854  0ebcd575d3c6 
parent 24242  e52ef498c0ba 
child 24960  39d1dd215d73 
permissions  rwrr 
23828  1 
(* Title: Pure/pure_setup.ML 
2 
ID: $Id$ 

3 
Author: Makarius 

4 

24053
af1dd276fae0
added ML toplevel use commands: Toplevel.program;
wenzelm
parents:
23828
diff
changeset

5 
Pure theory and ML toplevel setup. 
23828  6 
*) 
7 

24053
af1dd276fae0
added ML toplevel use commands: Toplevel.program;
wenzelm
parents:
23828
diff
changeset

8 
(* ML toplevel use commands *) 
af1dd276fae0
added ML toplevel use commands: Toplevel.program;
wenzelm
parents:
23828
diff
changeset

9 

af1dd276fae0
added ML toplevel use commands: Toplevel.program;
wenzelm
parents:
23828
diff
changeset

10 
fun use name = Toplevel.program (fn () => ThyInfo.use name); 
af1dd276fae0
added ML toplevel use commands: Toplevel.program;
wenzelm
parents:
23828
diff
changeset

11 
fun use_thys name = Toplevel.program (fn () => ThyInfo.use_thys name); 
af1dd276fae0
added ML toplevel use commands: Toplevel.program;
wenzelm
parents:
23828
diff
changeset

12 
fun use_thy name = Toplevel.program (fn () => ThyInfo.use_thy name); 
24174
59a5ffec7078
theory loader: removed obsolete update_thy (coincides with use_thy);
wenzelm
parents:
24053
diff
changeset

13 
fun time_use name = Toplevel.program (fn () => ThyInfo.time_use name); 
24053
af1dd276fae0
added ML toplevel use commands: Toplevel.program;
wenzelm
parents:
23828
diff
changeset

14 
fun time_use_thy name = Toplevel.program (fn () => ThyInfo.time_use_thy name); 
af1dd276fae0
added ML toplevel use commands: Toplevel.program;
wenzelm
parents:
23828
diff
changeset

15 

af1dd276fae0
added ML toplevel use commands: Toplevel.program;
wenzelm
parents:
23828
diff
changeset

16 

af1dd276fae0
added ML toplevel use commands: Toplevel.program;
wenzelm
parents:
23828
diff
changeset

17 
(* the Pure theories *) 
af1dd276fae0
added ML toplevel use commands: Toplevel.program;
wenzelm
parents:
23828
diff
changeset

18 

23828  19 
use_thy "Pure"; 
20 
structure Pure = struct val thy = theory "Pure" end; 

21 

22 
Context.add_setup 

24242  23 
(Sign.del_modesyntax_i Syntax.default_mode PureThy.appl_syntax #> 
24 
Sign.add_syntax_i PureThy.applC_syntax); 

23828  25 
use_thy "CPure"; 
26 
structure CPure = struct val thy = theory "CPure" end; 

27 

24053
af1dd276fae0
added ML toplevel use commands: Toplevel.program;
wenzelm
parents:
23828
diff
changeset

28 

af1dd276fae0
added ML toplevel use commands: Toplevel.program;
wenzelm
parents:
23828
diff
changeset

29 
(* ML toplevel pretty printing *) 
af1dd276fae0
added ML toplevel use commands: Toplevel.program;
wenzelm
parents:
23828
diff
changeset

30 

af1dd276fae0
added ML toplevel use commands: Toplevel.program;
wenzelm
parents:
23828
diff
changeset

31 
install_pp (make_pp ["Thm", "thm"] ProofDisplay.pprint_thm); 
af1dd276fae0
added ML toplevel use commands: Toplevel.program;
wenzelm
parents:
23828
diff
changeset

32 
install_pp (make_pp ["Thm", "cterm"] ProofDisplay.pprint_cterm); 
af1dd276fae0
added ML toplevel use commands: Toplevel.program;
wenzelm
parents:
23828
diff
changeset

33 
install_pp (make_pp ["Thm", "ctyp"] ProofDisplay.pprint_ctyp); 
af1dd276fae0
added ML toplevel use commands: Toplevel.program;
wenzelm
parents:
23828
diff
changeset

34 
install_pp (make_pp ["Context", "theory"] Context.pprint_thy); 
af1dd276fae0
added ML toplevel use commands: Toplevel.program;
wenzelm
parents:
23828
diff
changeset

35 
install_pp (make_pp ["Context", "proof"] ProofDisplay.pprint_context); 
af1dd276fae0
added ML toplevel use commands: Toplevel.program;
wenzelm
parents:
23828
diff
changeset

36 
install_pp (make_pp ["Syntax", "ast"] Syntax.pprint_ast); 
af1dd276fae0
added ML toplevel use commands: Toplevel.program;
wenzelm
parents:
23828
diff
changeset

37 
install_pp (make_pp ["typ"] (ProofDisplay.pprint_typ Pure.thy)); 
af1dd276fae0
added ML toplevel use commands: Toplevel.program;
wenzelm
parents:
23828
diff
changeset

38 
install_pp (make_pp ["Path", "T"] (Pretty.pprint o Pretty.str o quote o Path.implode)); 
af1dd276fae0
added ML toplevel use commands: Toplevel.program;
wenzelm
parents:
23828
diff
changeset

39 
install_pp (make_pp ["File", "ident"] (Pretty.pprint o Pretty.str o quote o File.rep_ident)); 
af1dd276fae0
added ML toplevel use commands: Toplevel.program;
wenzelm
parents:
23828
diff
changeset

40 

af1dd276fae0
added ML toplevel use commands: Toplevel.program;
wenzelm
parents:
23828
diff
changeset

41 

af1dd276fae0
added ML toplevel use commands: Toplevel.program;
wenzelm
parents:
23828
diff
changeset

42 
(* misc *) 
af1dd276fae0
added ML toplevel use commands: Toplevel.program;
wenzelm
parents:
23828
diff
changeset

43 

23828  44 
val cd = File.cd o Path.explode; 
45 
ml_prompts "ML> " "ML# "; 

46 

47 
proofs := 0; 