author  wenzelm 
Sun, 18 May 2008 17:03:20 +0200  
changeset 26957  e3f04fdd994d 
parent 26608  ff838a61dad6 
child 27341  97e2ccba3b64 
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 

26608  19 
val theory = ThyInfo.get_theory; 
20 

26463  21 
Context.>> (Context.map_theory 
22 
(OuterSyntax.process_file (Path.explode "Pure.thy") #> 

23 
Theory.end_theory)); 

26427  24 
structure Pure = struct val thy = ML_Context.the_global_context () end; 
25 
Context.set_thread_data NONE; 

26 
ThyInfo.register_theory Pure.thy; 

23828  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 

25223  47 
Proofterm.proofs := 0; 