src/Pure/Isar/isar_cmd.ML
author wenzelm
Tue Dec 05 22:14:42 2006 +0100 (2006-12-05)
changeset 21658 5e31241e1e3c
parent 21566 af2932baf068
child 21663 734a9c3f562d
permissions -rw-r--r--
Attrib.internal: morphism;
     1 (*  Title:      Pure/Isar/isar_cmd.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4 
     5 Derived Isar commands.
     6 *)
     7 
     8 signature ISAR_CMD =
     9 sig
    10   val add_axioms: ((bstring * string) * Attrib.src list) list -> theory -> theory
    11   val add_defs: (bool * bool) * ((bstring * string) * Attrib.src list) list -> theory -> theory
    12   val apply_theorems: (thmref * Attrib.src list) list -> theory -> thm list * theory
    13   val apply_theorems_i: (thm list * attribute list) list -> theory -> thm list * theory
    14   val have: ((string * Attrib.src list) * (string * string list) list) list ->
    15     bool -> Proof.state -> Proof.state
    16   val hence: ((string * Attrib.src list) * (string * string list) list) list ->
    17     bool -> Proof.state -> Proof.state
    18   val show: ((string * Attrib.src list) * (string * string list) list) list ->
    19     bool -> Proof.state -> Proof.state
    20   val thus: ((string * Attrib.src list) * (string * string list) list) list ->
    21     bool -> Proof.state -> Proof.state
    22   val qed: Method.text option -> Toplevel.transition -> Toplevel.transition
    23   val terminal_proof: Method.text * Method.text option ->
    24     Toplevel.transition -> Toplevel.transition
    25   val default_proof: Toplevel.transition -> Toplevel.transition
    26   val immediate_proof: Toplevel.transition -> Toplevel.transition
    27   val done_proof: Toplevel.transition -> Toplevel.transition
    28   val skip_proof: Toplevel.transition -> Toplevel.transition
    29   val begin_theory: string -> string list -> (string * bool) list -> bool -> theory
    30   val end_theory: theory -> theory
    31   val kill_theory: string -> unit
    32   val theory: string * string list * (string * bool) list
    33     -> Toplevel.transition -> Toplevel.transition
    34   val init_context: ('a -> unit) -> 'a -> Toplevel.transition -> Toplevel.transition
    35   val welcome: Toplevel.transition -> Toplevel.transition
    36   val init_toplevel: Toplevel.transition -> Toplevel.transition
    37   val exit: Toplevel.transition -> Toplevel.transition
    38   val quit: Toplevel.transition -> Toplevel.transition
    39   val touch_child_thys: string -> Toplevel.transition -> Toplevel.transition
    40   val touch_all_thys: Toplevel.transition -> Toplevel.transition
    41   val touch_thy: string -> Toplevel.transition -> Toplevel.transition
    42   val remove_thy: string -> Toplevel.transition -> Toplevel.transition
    43   val kill_thy: string -> Toplevel.transition -> Toplevel.transition
    44   val pr: string list * (int option * int option) -> Toplevel.transition -> Toplevel.transition
    45   val disable_pr: Toplevel.transition -> Toplevel.transition
    46   val enable_pr: Toplevel.transition -> Toplevel.transition
    47   val cannot_undo: string -> Toplevel.transition -> Toplevel.transition
    48   val clear_undos_theory: int -> Toplevel.transition -> Toplevel.transition
    49   val redo: Toplevel.transition -> Toplevel.transition
    50   val undos_proof: int -> Toplevel.transition -> Toplevel.transition
    51   val kill_proof_notify: (unit -> unit) -> Toplevel.transition -> Toplevel.transition
    52   val kill_proof: Toplevel.transition -> Toplevel.transition
    53   val undo_theory: Toplevel.transition -> Toplevel.transition
    54   val undo: Toplevel.transition -> Toplevel.transition
    55   val kill: Toplevel.transition -> Toplevel.transition
    56   val back: Toplevel.transition -> Toplevel.transition
    57   val use: Path.T -> Toplevel.transition -> Toplevel.transition
    58   val use_mltext_theory: string -> Toplevel.transition -> Toplevel.transition
    59   val use_mltext: bool -> string -> Toplevel.transition -> Toplevel.transition
    60   val use_commit: Toplevel.transition -> Toplevel.transition
    61   val cd: Path.T -> Toplevel.transition -> Toplevel.transition
    62   val pwd: Toplevel.transition -> Toplevel.transition
    63   val use_thy: string -> Toplevel.transition -> Toplevel.transition
    64   val use_thy_only: string -> Toplevel.transition -> Toplevel.transition
    65   val update_thy: string -> Toplevel.transition -> Toplevel.transition
    66   val update_thy_only: string -> Toplevel.transition -> Toplevel.transition
    67   val display_drafts: Path.T list -> Toplevel.transition -> Toplevel.transition
    68   val print_drafts: Path.T list -> Toplevel.transition -> Toplevel.transition
    69   val pretty_setmargin: int -> Toplevel.transition -> Toplevel.transition
    70   val print_context: Toplevel.transition -> Toplevel.transition
    71   val print_theory: bool -> Toplevel.transition -> Toplevel.transition
    72   val print_syntax: Toplevel.transition -> Toplevel.transition
    73   val print_facts: Toplevel.transition -> Toplevel.transition
    74   val print_theorems: Toplevel.transition -> Toplevel.transition
    75   val print_locales: Toplevel.transition -> Toplevel.transition
    76   val print_locale: bool * (Locale.expr * Element.context list)
    77     -> Toplevel.transition -> Toplevel.transition
    78   val print_registrations: bool -> string -> Toplevel.transition -> Toplevel.transition
    79   val print_attributes: Toplevel.transition -> Toplevel.transition
    80   val print_simpset: Toplevel.transition -> Toplevel.transition
    81   val print_rules: Toplevel.transition -> Toplevel.transition
    82   val print_induct_rules: Toplevel.transition -> Toplevel.transition
    83   val print_trans_rules: Toplevel.transition -> Toplevel.transition
    84   val print_methods: Toplevel.transition -> Toplevel.transition
    85   val print_antiquotations: Toplevel.transition -> Toplevel.transition
    86   val class_deps: Toplevel.transition -> Toplevel.transition
    87   val thm_deps: (thmref * Attrib.src list) list -> Toplevel.transition -> Toplevel.transition
    88   val find_theorems: int option * (bool * string FindTheorems.criterion) list
    89     -> Toplevel.transition -> Toplevel.transition
    90   val print_binds: Toplevel.transition -> Toplevel.transition
    91   val print_cases: Toplevel.transition -> Toplevel.transition
    92   val print_stmts: string list * (thmref * Attrib.src list) list
    93     -> Toplevel.transition -> Toplevel.transition
    94   val print_thms: string list * (thmref * Attrib.src list) list
    95     -> Toplevel.transition -> Toplevel.transition
    96   val print_prfs: bool -> string list * (thmref * Attrib.src list) list option
    97     -> Toplevel.transition -> Toplevel.transition
    98   val print_prop: (string list * string) -> Toplevel.transition -> Toplevel.transition
    99   val print_term: (string list * string) -> Toplevel.transition -> Toplevel.transition
   100   val print_type: (string list * string) -> Toplevel.transition -> Toplevel.transition
   101   val add_header: string * Position.T -> Toplevel.transition -> Toplevel.transition
   102   val add_chapter: xstring option * (string * Position.T) ->
   103     Toplevel.transition -> Toplevel.transition
   104   val add_section: xstring option * (string * Position.T) ->
   105     Toplevel.transition -> Toplevel.transition
   106   val add_subsection: xstring option * (string * Position.T) ->
   107     Toplevel.transition -> Toplevel.transition
   108   val add_subsubsection: xstring option * (string * Position.T) ->
   109     Toplevel.transition -> Toplevel.transition
   110   val add_text: xstring option * (string * Position.T) ->
   111     Toplevel.transition -> Toplevel.transition
   112   val add_text_raw: string * Position.T -> Toplevel.transition -> Toplevel.transition
   113   val add_sect: string * Position.T -> Toplevel.transition -> Toplevel.transition
   114   val add_subsect: string * Position.T -> Toplevel.transition -> Toplevel.transition
   115   val add_subsubsect: string * Position.T -> Toplevel.transition -> Toplevel.transition
   116   val add_txt: string * Position.T -> Toplevel.transition -> Toplevel.transition
   117   val add_txt_raw: string * Position.T -> Toplevel.transition -> Toplevel.transition
   118 end;
   119 
   120 structure IsarCmd: ISAR_CMD =
   121 struct
   122 
   123 
   124 (* axioms *)
   125 
   126 fun add_axms f args thy =
   127   f (map (fn (x, srcs) => (x, map (Attrib.attribute thy) srcs)) args) thy;
   128 
   129 val add_axioms = add_axms (snd oo PureThy.add_axioms);
   130 
   131 fun add_defs ((unchecked, overloaded), args) =
   132   add_axms
   133     (snd oo (if unchecked then PureThy.add_defs_unchecked else PureThy.add_defs) overloaded) args;
   134 
   135 
   136 (* facts *)
   137 
   138 fun apply_theorems args thy =
   139   let val facts = Attrib.map_facts (Attrib.attribute thy) [(("", []), args)]
   140   in apfst (maps snd) (PureThy.note_thmss "" facts thy) end;
   141 
   142 fun apply_theorems_i args = apfst (maps snd) o PureThy.note_thmss_i "" [(("", []), args)];
   143 
   144 
   145 (* goals *)
   146 
   147 fun goal opt_chain goal stmt int =
   148   opt_chain #> goal NONE (K Seq.single) stmt int;
   149 
   150 val have = goal I Proof.have;
   151 val hence = goal Proof.chain Proof.have;
   152 val show = goal I Proof.show;
   153 val thus = goal Proof.chain Proof.show;
   154 
   155 
   156 (* local endings *)
   157 
   158 fun local_qed m = Toplevel.proofs (Proof.local_qed (m, true));
   159 val local_terminal_proof = Toplevel.proofs o Proof.local_terminal_proof;
   160 val local_default_proof = Toplevel.proofs Proof.local_default_proof;
   161 val local_immediate_proof = Toplevel.proofs Proof.local_immediate_proof;
   162 val local_done_proof = Toplevel.proofs Proof.local_done_proof;
   163 val local_skip_proof = Toplevel.proofs' Proof.local_skip_proof;
   164 
   165 val skip_local_qed =
   166   Toplevel.skip_proof (History.apply (fn i => if i > 1 then i - 1 else raise Toplevel.UNDEF));
   167 
   168 
   169 (* global endings *)
   170 
   171 fun global_qed m = Toplevel.end_proof (K (Proof.global_qed (m, true)));
   172 val global_terminal_proof = Toplevel.end_proof o K o Proof.global_terminal_proof;
   173 val global_default_proof = Toplevel.end_proof (K Proof.global_default_proof);
   174 val global_immediate_proof = Toplevel.end_proof (K Proof.global_immediate_proof);
   175 val global_skip_proof = Toplevel.end_proof Proof.global_skip_proof;
   176 val global_done_proof = Toplevel.end_proof (K Proof.global_done_proof);
   177 
   178 val skip_global_qed = Toplevel.skip_proof_to_theory (equal 1);
   179 
   180 
   181 (* common endings *)
   182 
   183 fun qed m = local_qed m o global_qed m o skip_local_qed o skip_global_qed;
   184 fun terminal_proof m = local_terminal_proof m o global_terminal_proof m;
   185 val default_proof = local_default_proof o global_default_proof;
   186 val immediate_proof = local_immediate_proof o global_immediate_proof;
   187 val done_proof = local_done_proof o global_done_proof;
   188 val skip_proof = local_skip_proof o global_skip_proof;
   189 
   190 
   191 (* init and exit *)
   192 
   193 fun begin_theory name imports uses =
   194   ThyInfo.begin_theory Present.begin_theory name imports (map (apfst Path.unpack) uses);
   195 
   196 fun end_theory thy =
   197   if ThyInfo.check_known_thy (Context.theory_name thy) then ThyInfo.end_theory thy else thy;
   198 
   199 val kill_theory = ThyInfo.if_known_thy ThyInfo.remove_thy;
   200 
   201 fun theory (name, imports, uses) =
   202   Toplevel.init_theory (begin_theory name imports uses)
   203     (fn thy => (end_theory thy; ()))
   204     (kill_theory o Context.theory_name);
   205 
   206 fun init_context f x = Toplevel.init_theory
   207   (fn _ =>
   208     (case Context.pass NONE f x of
   209       ((), NONE) => raise Toplevel.UNDEF
   210     | ((), SOME thy) => thy))
   211   (K ()) (K ());
   212 
   213 val init_toplevel = Toplevel.imperative (fn () => raise Toplevel.RESTART);
   214 
   215 val welcome = Toplevel.imperative (writeln o Session.welcome);
   216 
   217 val exit = Toplevel.keep (fn state =>
   218   (Context.set_context (try Toplevel.theory_of state);
   219     writeln "Leaving the Isar loop.  Invoke 'Isar.loop();' to continue.";
   220     raise Toplevel.TERMINATE));
   221 
   222 val quit = Toplevel.imperative quit;
   223 
   224 
   225 (* touch theories *)
   226 
   227 fun touch_child_thys name = Toplevel.imperative (fn () => ThyInfo.touch_child_thys name);
   228 val touch_all_thys = Toplevel.imperative ThyInfo.touch_all_thys;
   229 fun touch_thy name = Toplevel.imperative (fn () => ThyInfo.touch_thy name);
   230 fun remove_thy name = Toplevel.imperative (fn () => ThyInfo.remove_thy name);
   231 fun kill_thy name = Toplevel.imperative (fn () => kill_theory name);
   232 
   233 
   234 (* print state *)
   235 
   236 fun with_modes modes e =
   237   Library.setmp print_mode (modes @ ! print_mode) e ();
   238 
   239 fun set_limit _ NONE = ()
   240   | set_limit r (SOME n) = r := n;
   241 
   242 fun pr (modes, (lim1, lim2)) = Toplevel.keep (fn state =>
   243   (set_limit goals_limit lim1; set_limit ProofContext.prems_limit lim2; Toplevel.quiet := false;
   244     with_modes modes (fn () => Toplevel.print_state true state)));
   245 
   246 val disable_pr = Toplevel.imperative (fn () => Toplevel.quiet := true);
   247 val enable_pr = Toplevel.imperative (fn () => Toplevel.quiet := false);
   248 
   249 
   250 (* history commands *)
   251 
   252 fun cannot_undo txt = Toplevel.imperative (fn () => error ("Cannot undo " ^ quote txt));
   253 
   254 val clear_undos_theory = Toplevel.history o History.clear;
   255 
   256 val redo =
   257   Toplevel.history History.redo o
   258   Toplevel.actual_proof ProofHistory.redo o
   259   Toplevel.skip_proof History.redo;
   260 
   261 fun undos_proof n =
   262   Toplevel.actual_proof (fn prf =>
   263     if ProofHistory.is_initial prf then raise Toplevel.UNDEF else funpow n ProofHistory.undo prf) o
   264   Toplevel.skip_proof (fn h =>
   265     if History.is_initial h then raise Toplevel.UNDEF else funpow n History.undo h);
   266 
   267 fun kill_proof_notify (f: unit -> unit) = Toplevel.history (fn hist =>
   268   if is_some (Toplevel.theory_node (History.current hist)) then raise Toplevel.UNDEF
   269   else (f (); History.undo hist));
   270 
   271 val kill_proof = kill_proof_notify (K ());
   272 
   273 val undo_theory = Toplevel.history (fn hist =>
   274   if History.is_initial hist then raise Toplevel.UNDEF else History.undo hist);
   275 
   276 val undo = Toplevel.kill o undo_theory o undos_proof 1;
   277 val kill = Toplevel.kill o kill_proof;
   278 
   279 val back =
   280   Toplevel.actual_proof ProofHistory.back o
   281   Toplevel.skip_proof (History.apply I);
   282 
   283 
   284 (* use ML text *)
   285 
   286 fun use path = Toplevel.keep (fn state =>
   287   Context.setmp (try Toplevel.theory_of state) (ThyInfo.load_file false) path);
   288 
   289 (*passes changes of theory context*)
   290 val use_mltext_theory = Toplevel.theory' o Context.use_mltext_theory;
   291 
   292 (*ignore result theory context*)
   293 fun use_mltext v txt = Toplevel.keep' (fn verb => fn state =>
   294   (Context.use_mltext txt (v andalso verb) (try Toplevel.theory_of state)));
   295 
   296 val use_commit = Toplevel.imperative Secure.commit;
   297 
   298 
   299 (* current working directory *)
   300 
   301 fun cd path = Toplevel.imperative (fn () => (File.cd path));
   302 val pwd = Toplevel.imperative (fn () => writeln (Path.pack (File.pwd ())));
   303 
   304 
   305 (* load theory files *)
   306 
   307 fun use_thy name = Toplevel.imperative (fn () => Context.save ThyInfo.use_thy name);
   308 fun use_thy_only name = Toplevel.imperative (fn () => Context.save ThyInfo.use_thy_only name);
   309 fun update_thy name = Toplevel.imperative (fn () => Context.save ThyInfo.update_thy name);
   310 fun update_thy_only name =
   311   Toplevel.imperative (fn () => Context.save ThyInfo.update_thy_only name);
   312 
   313 
   314 (* present draft files *)
   315 
   316 fun display_drafts files = Toplevel.imperative (fn () =>
   317   let val outfile = File.shell_path (Present.drafts (getenv "ISABELLE_DOC_FORMAT") files)
   318   in File.isatool ("display -c " ^ outfile ^ " &"); () end);
   319 
   320 fun print_drafts files = Toplevel.imperative (fn () =>
   321   let val outfile = File.shell_path (Present.drafts "ps" files)
   322   in File.isatool ("print -c " ^ outfile); () end);
   323 
   324 
   325 (* pretty_setmargin *)
   326 
   327 fun pretty_setmargin n = Toplevel.imperative (fn () => Pretty.setmargin n);
   328 
   329 
   330 (* print parts of theory and proof context *)
   331 
   332 val print_context = Toplevel.keep Toplevel.print_state_context;
   333 
   334 fun print_theory verbose = Toplevel.unknown_theory o
   335   Toplevel.keep (ProofDisplay.print_full_theory verbose o Toplevel.theory_of);
   336 
   337 val print_syntax = Toplevel.unknown_theory o
   338   Toplevel.keep (Display.print_syntax o Toplevel.theory_of) o
   339   Toplevel.keep (ProofContext.print_syntax o Proof.context_of o Toplevel.proof_of);
   340 
   341 val print_facts = Toplevel.unknown_context o Toplevel.keep (fn state =>
   342   ProofContext.setmp_verbose
   343     ProofContext.print_lthms (Toplevel.context_of state));
   344 
   345 val print_theorems_proof = Toplevel.keep (fn state =>
   346   ProofContext.setmp_verbose
   347     ProofContext.print_lthms (Proof.context_of (Toplevel.proof_of state)));
   348 
   349 val print_theorems_theory = Toplevel.keep (fn state =>
   350   Toplevel.theory_of state |>
   351   (case Option.map Toplevel.theory_node (History.previous (Toplevel.node_history_of state)) of
   352     SOME (SOME prev_thy) => ProofDisplay.print_theorems_diff (Context.theory_of prev_thy)
   353   | _ => ProofDisplay.print_theorems));
   354 
   355 val print_theorems = Toplevel.unknown_theory o print_theorems_theory o print_theorems_proof;
   356 
   357 val print_locales = Toplevel.unknown_theory o
   358   Toplevel.keep (Locale.print_locales o Toplevel.theory_of);
   359 
   360 fun print_locale (show_facts, (import, body)) = Toplevel.unknown_theory o
   361   Toplevel.keep (fn state =>
   362     Locale.print_locale (Toplevel.theory_of state) show_facts import body);
   363 
   364 fun print_registrations show_wits name = Toplevel.unknown_context o
   365   Toplevel.keep (Toplevel.node_case
   366       (Context.cases (Locale.print_global_registrations show_wits name)
   367         (Locale.print_local_registrations show_wits name))
   368     (Locale.print_local_registrations show_wits name o Proof.context_of));
   369 
   370 val print_attributes = Toplevel.unknown_theory o
   371   Toplevel.keep (Attrib.print_attributes o Toplevel.theory_of);
   372 
   373 val print_simpset = Toplevel.unknown_context o
   374   Toplevel.keep (Toplevel.node_case
   375     (Context.cases Simplifier.print_simpset Simplifier.print_local_simpset)
   376     (Simplifier.print_local_simpset o Proof.context_of));
   377 
   378 val print_rules = Toplevel.unknown_context o
   379   Toplevel.keep (ContextRules.print_rules o Toplevel.context_of);
   380 
   381 val print_induct_rules = Toplevel.unknown_context o
   382   Toplevel.keep (InductAttrib.print_rules o Toplevel.context_of);
   383 
   384 val print_trans_rules = Toplevel.unknown_context o
   385   Toplevel.keep (Calculation.print_rules o Toplevel.context_of);
   386 
   387 val print_methods = Toplevel.unknown_theory o
   388   Toplevel.keep (Method.print_methods o Toplevel.theory_of);
   389 
   390 val print_antiquotations = Toplevel.imperative IsarOutput.print_antiquotations;
   391 
   392 val class_deps = Toplevel.unknown_theory o Toplevel.keep (fn state =>
   393   let
   394     val thy = Toplevel.theory_of state;
   395     val {classes = (space, algebra), ...} = Type.rep_tsig (Sign.tsig_of thy);
   396     val {classes, ...} = Sorts.rep_algebra algebra;
   397     fun entry (c, (i, (_, cs))) =
   398       (i, {name = NameSpace.extern space c, ID = c, parents = cs,
   399             dir = "", unfold = true, path = ""});
   400     val gr =
   401       Graph.fold (cons o entry) classes []
   402       |> sort (int_ord o pairself #1) |> map #2;
   403   in Present.display_graph gr end);
   404 
   405 
   406 (* retrieve theorems *)
   407 
   408 fun thm_deps args = Toplevel.unknown_theory o Toplevel.keep (fn state =>
   409   ThmDeps.thm_deps (Proof.get_thmss (Toplevel.enter_proof_body state) args));
   410 
   411 fun find_theorems (opt_lim, spec) = Toplevel.unknown_theory o Toplevel.keep (fn state =>
   412   let
   413     val proof_state = Toplevel.enter_proof_body state;
   414     val ctxt = Proof.context_of proof_state;
   415     val opt_goal = try Proof.get_goal proof_state |> Option.map (Thm.prop_of o #2 o #2);
   416   in FindTheorems.print_theorems ctxt opt_goal opt_lim spec end);
   417 
   418 
   419 (* print proof context contents *)
   420 
   421 val print_binds = Toplevel.unknown_proof o Toplevel.keep (fn state =>
   422   ProofContext.setmp_verbose
   423     ProofContext.print_binds (Proof.context_of (Toplevel.proof_of state)));
   424 
   425 val print_cases = Toplevel.unknown_proof o Toplevel.keep (fn state =>
   426   ProofContext.setmp_verbose
   427     ProofContext.print_cases (Proof.context_of (Toplevel.proof_of state)));
   428 
   429 
   430 (* print theorems, terms, types etc. *)
   431 
   432 local
   433 
   434 fun string_of_stmts state args =
   435   Proof.get_thmss state args
   436   |> map (Element.pretty_statement (Proof.context_of state) Thm.theoremK)
   437   |> Pretty.chunks2 |> Pretty.string_of;
   438 
   439 fun string_of_thms state args =
   440   Pretty.string_of (ProofContext.pretty_thms (Proof.context_of state)
   441     (Proof.get_thmss state args));
   442 
   443 fun string_of_prfs full state arg =
   444   Pretty.string_of (case arg of
   445       NONE =>
   446         let
   447           val (ctxt, (_, thm)) = Proof.get_goal state;
   448           val {thy, der = (_, prf), ...} = Thm.rep_thm thm;
   449           val prop = Thm.full_prop_of thm;
   450           val prf' = Proofterm.rewrite_proof_notypes ([], []) prf
   451         in
   452           ProofContext.pretty_proof ctxt
   453             (if full then Reconstruct.reconstruct_proof thy prop prf' else prf')
   454         end
   455     | SOME args => Pretty.chunks
   456         (map (ProofContext.pretty_proof_of (Proof.context_of state) full)
   457           (Proof.get_thmss state args)));
   458 
   459 fun string_of_prop state s =
   460   let
   461     val ctxt = Proof.context_of state;
   462     val prop = ProofContext.read_prop ctxt s;
   463   in Pretty.string_of (Pretty.quote (ProofContext.pretty_term ctxt prop)) end;
   464 
   465 fun string_of_term state s =
   466   let
   467     val ctxt = Proof.context_of state;
   468     val t = ProofContext.read_term ctxt s;
   469     val T = Term.type_of t;
   470   in
   471     Pretty.string_of
   472       (Pretty.block [Pretty.quote (ProofContext.pretty_term ctxt t), Pretty.fbrk,
   473         Pretty.str "::", Pretty.brk 1, Pretty.quote (ProofContext.pretty_typ ctxt T)])
   474   end;
   475 
   476 fun string_of_type state s =
   477   let
   478     val ctxt = Proof.context_of state;
   479     val T = ProofContext.read_typ ctxt s;
   480   in Pretty.string_of (Pretty.quote (ProofContext.pretty_typ ctxt T)) end;
   481 
   482 fun print_item string_of (modes, arg) = Toplevel.keep (fn state => with_modes modes (fn () =>
   483   writeln (string_of (Toplevel.enter_proof_body state) arg)));
   484 
   485 in
   486 
   487 val print_stmts = print_item string_of_stmts;
   488 val print_thms = print_item string_of_thms;
   489 val print_prfs = print_item o string_of_prfs;
   490 val print_prop = print_item string_of_prop;
   491 val print_term = print_item string_of_term;
   492 val print_type = print_item string_of_type;
   493 
   494 end;
   495 
   496 
   497 (* markup commands *)
   498 
   499 fun add_header s = Toplevel.keep' (fn int => fn state =>
   500   (Toplevel.assert (Toplevel.is_toplevel state);
   501    if int then OuterSyntax.check_text s NONE else ()));
   502 
   503 local
   504 
   505 fun present _ txt true node = OuterSyntax.check_text txt (SOME node)
   506   | present f (s, _) false node =
   507       Context.setmp (try (Toplevel.cases_node Context.theory_of Proof.theory_of) node) f s;
   508 
   509 fun present_local_theory f (loc, txt) = Toplevel.present_local_theory loc (present f txt);
   510 fun present_proof f txt = Toplevel.print o Toplevel.present_proof (present f txt);
   511 
   512 in
   513 
   514 val add_chapter       = present_local_theory Present.section;
   515 val add_section       = present_local_theory Present.section;
   516 val add_subsection    = present_local_theory Present.subsection;
   517 val add_subsubsection = present_local_theory Present.subsubsection;
   518 val add_text          = present_local_theory (K ());
   519 fun add_text_raw txt  = present_local_theory (K ()) (NONE, txt);
   520 val add_txt           = present_proof (K ());
   521 val add_txt_raw       = add_txt;
   522 val add_sect          = add_txt;
   523 val add_subsect       = add_txt;
   524 val add_subsubsect    = add_txt;
   525 
   526 end;
   527 
   528 end;