25 ThyInfo.register_theory Pure.thy; |
25 ThyInfo.register_theory Pure.thy; |
26 |
26 |
27 |
27 |
28 (* ML toplevel pretty printing *) |
28 (* ML toplevel pretty printing *) |
29 |
29 |
30 install_pp (make_pp ["Task_Queue", "task"] (Pretty.pprint o Pretty.str o Task_Queue.str_of_task)); |
30 toplevel_pp ["Task_Queue", "task"] "Pretty.str o Task_Queue.str_of_task"; |
31 install_pp (make_pp ["Task_Queue", "group"] (Pretty.pprint o Pretty.str o Task_Queue.str_of_group)); |
31 toplevel_pp ["Task_Queue", "group"] "Pretty.str o Task_Queue.str_of_group"; |
32 install_pp (make_pp ["Position", "T"] (Pretty.pprint o Pretty.position)); |
32 toplevel_pp ["Position", "T"] "Pretty.position"; |
33 install_pp (make_pp ["Thm", "thm"] ProofDisplay.pprint_thm); |
33 toplevel_pp ["Binding", "binding"] "Pretty.str o quote o Binding.str_of"; |
34 install_pp (make_pp ["Thm", "cterm"] ProofDisplay.pprint_cterm); |
34 toplevel_pp ["Thm", "thm"] "ProofDisplay.pp_thm"; |
35 install_pp (make_pp ["Binding", "binding"] (Pretty.pprint o Pretty.str o quote o Binding.str_of)); |
35 toplevel_pp ["Thm", "cterm"] "ProofDisplay.pp_cterm"; |
36 install_pp (make_pp ["Thm", "ctyp"] ProofDisplay.pprint_ctyp); |
36 toplevel_pp ["Thm", "ctyp"] "ProofDisplay.pp_ctyp"; |
37 install_pp (make_pp ["Context", "theory"] Context.pprint_thy); |
37 toplevel_pp ["typ"] "ProofDisplay.pp_typ Pure.thy"; |
38 install_pp (make_pp ["Context", "theory_ref"] Context.pprint_thy_ref); |
38 toplevel_pp ["Context", "theory"] "Context.pretty_thy"; |
39 install_pp (make_pp ["Context", "proof"] ProofDisplay.pprint_context); |
39 toplevel_pp ["Context", "theory_ref"] "Context.pretty_thy o Theory.deref"; |
40 install_pp (make_pp ["Syntax", "ast"] Syntax.pprint_ast); |
40 toplevel_pp ["Context", "proof"] "ProofDisplay.pp_context"; |
41 install_pp (make_pp ["typ"] (ProofDisplay.pprint_typ Pure.thy)); |
41 toplevel_pp ["Syntax", "ast"] "Syntax.pretty_ast"; |
42 install_pp (make_pp ["Path", "T"] (Pretty.pprint o Pretty.str o quote o Path.implode)); |
42 toplevel_pp ["Path", "T"] "Pretty.str o quote o Path.implode"; |
43 install_pp (make_pp ["File", "ident"] (Pretty.pprint o Pretty.str o quote o File.rep_ident)); |
43 toplevel_pp ["File", "ident"] "Pretty.str o quote o File.rep_ident"; |
44 |
44 |
45 if File.exists (Path.explode ("ML-Systems/install_pp_" ^ ml_system ^ ".ML")) then |
45 if File.exists (Path.explode ("ML-Systems/install_pp_" ^ ml_system ^ ".ML")) |
46 use ("ML-Systems/install_pp_" ^ ml_system ^ ".ML") |
46 then use ("ML-Systems/install_pp_" ^ ml_system ^ ".ML") |
47 else if String.isPrefix "polyml" ml_system then use "ML-Systems/install_pp_polyml.ML" |
47 else if String.isPrefix "polyml" ml_system |
|
48 then use "ML-Systems/install_pp_polyml.ML" |
48 else (); |
49 else (); |
49 |
50 |
50 |
51 |
51 (* misc *) |
52 (* misc *) |
52 |
53 |