src/Pure/Isar/isar_cmd.ML
author wenzelm
Fri Aug 24 12:35:39 2012 +0200 (2012-08-24 ago)
changeset 48918 6e5fd4585512
parent 48881 46e053eda5dd
child 49012 8686c36fa27d
permissions -rw-r--r--
check side-comments of command spans (normally filtered out in Outer_Syntax.toplevel_source);
     1 (*  Title:      Pure/Isar/isar_cmd.ML
     2     Author:     Markus Wenzel, TU Muenchen
     3 
     4 Miscellaneous Isar commands.
     5 *)
     6 
     7 signature ISAR_CMD =
     8 sig
     9   val global_setup: Symbol_Pos.text * Position.T -> theory -> theory
    10   val local_setup: Symbol_Pos.text * Position.T -> Proof.context -> Proof.context
    11   val parse_ast_translation: bool * (Symbol_Pos.text * Position.T) -> theory -> theory
    12   val parse_translation: bool * (Symbol_Pos.text * Position.T) -> theory -> theory
    13   val print_translation: bool * (Symbol_Pos.text * Position.T) -> theory -> theory
    14   val typed_print_translation: bool * (Symbol_Pos.text * Position.T) -> theory -> theory
    15   val print_ast_translation: bool * (Symbol_Pos.text * Position.T) -> theory -> theory
    16   val translations: (xstring * string) Syntax.trrule list -> theory -> theory
    17   val no_translations: (xstring * string) Syntax.trrule list -> theory -> theory
    18   val oracle: bstring * Position.T -> Symbol_Pos.text * Position.T -> theory -> theory
    19   val add_axioms: (Attrib.binding * string) list -> theory -> theory
    20   val add_defs: (bool * bool) * ((binding * string) * Attrib.src list) list -> theory -> theory
    21   val declaration: {syntax: bool, pervasive: bool} ->
    22     Symbol_Pos.text * Position.T -> local_theory -> local_theory
    23   val simproc_setup: string * Position.T -> string list -> Symbol_Pos.text * Position.T ->
    24     string list -> local_theory -> local_theory
    25   val hide_class: bool -> xstring list -> theory -> theory
    26   val hide_type: bool -> xstring list -> theory -> theory
    27   val hide_const: bool -> xstring list -> theory -> theory
    28   val hide_fact: bool -> xstring list -> theory -> theory
    29   val have: (Attrib.binding * (string * string list) list) list -> bool -> Proof.state -> Proof.state
    30   val hence: (Attrib.binding * (string * string list) list) list -> bool -> Proof.state -> Proof.state
    31   val show: (Attrib.binding * (string * string list) list) list -> bool -> Proof.state -> Proof.state
    32   val thus: (Attrib.binding * (string * string list) list) list -> bool -> Proof.state -> Proof.state
    33   val qed: Method.text option -> Toplevel.transition -> Toplevel.transition
    34   val terminal_proof: Method.text * Method.text option ->
    35     Toplevel.transition -> Toplevel.transition
    36   val default_proof: Toplevel.transition -> Toplevel.transition
    37   val immediate_proof: Toplevel.transition -> Toplevel.transition
    38   val done_proof: Toplevel.transition -> Toplevel.transition
    39   val skip_proof: Toplevel.transition -> Toplevel.transition
    40   val ml_diag: bool -> Symbol_Pos.text * Position.T -> Toplevel.transition -> Toplevel.transition
    41   val diag_state: Proof.context -> Toplevel.state
    42   val diag_goal: Proof.context -> {context: Proof.context, facts: thm list, goal: thm}
    43   val display_drafts: string list -> Toplevel.transition -> Toplevel.transition
    44   val print_drafts: string list -> Toplevel.transition -> Toplevel.transition
    45   val print_context: Toplevel.transition -> Toplevel.transition
    46   val print_theory: bool -> Toplevel.transition -> Toplevel.transition
    47   val print_syntax: Toplevel.transition -> Toplevel.transition
    48   val print_abbrevs: Toplevel.transition -> Toplevel.transition
    49   val print_facts: Toplevel.transition -> Toplevel.transition
    50   val print_configs: Toplevel.transition -> Toplevel.transition
    51   val print_theorems: bool -> Toplevel.transition -> Toplevel.transition
    52   val print_locales: Toplevel.transition -> Toplevel.transition
    53   val print_locale: bool * (xstring * Position.T) -> Toplevel.transition -> Toplevel.transition
    54   val print_registrations: xstring * Position.T -> Toplevel.transition -> Toplevel.transition
    55   val print_dependencies: bool * Expression.expression -> Toplevel.transition
    56     -> Toplevel.transition
    57   val print_attributes: Toplevel.transition -> Toplevel.transition
    58   val print_simpset: Toplevel.transition -> Toplevel.transition
    59   val print_rules: Toplevel.transition -> Toplevel.transition
    60   val print_trans_rules: Toplevel.transition -> Toplevel.transition
    61   val print_methods: Toplevel.transition -> Toplevel.transition
    62   val print_antiquotations: Toplevel.transition -> Toplevel.transition
    63   val class_deps: Toplevel.transition -> Toplevel.transition
    64   val thy_deps: Toplevel.transition -> Toplevel.transition
    65   val thm_deps: (Facts.ref * Attrib.src list) list -> Toplevel.transition -> Toplevel.transition
    66   val unused_thms: (string list * string list option) option ->
    67     Toplevel.transition -> Toplevel.transition
    68   val print_binds: Toplevel.transition -> Toplevel.transition
    69   val print_cases: Toplevel.transition -> Toplevel.transition
    70   val print_stmts: string list * (Facts.ref * Attrib.src list) list
    71     -> Toplevel.transition -> Toplevel.transition
    72   val print_thms: string list * (Facts.ref * Attrib.src list) list
    73     -> Toplevel.transition -> Toplevel.transition
    74   val print_prfs: bool -> string list * (Facts.ref * Attrib.src list) list option
    75     -> Toplevel.transition -> Toplevel.transition
    76   val print_prop: (string list * string) -> Toplevel.transition -> Toplevel.transition
    77   val print_term: (string list * string) -> Toplevel.transition -> Toplevel.transition
    78   val print_type: (string list * (string * string option)) ->
    79     Toplevel.transition -> Toplevel.transition
    80   val header_markup: Symbol_Pos.text * Position.T -> Toplevel.transition -> Toplevel.transition
    81   val local_theory_markup: (xstring * Position.T) option * (Symbol_Pos.text * Position.T) ->
    82     Toplevel.transition -> Toplevel.transition
    83   val proof_markup: Symbol_Pos.text * Position.T -> Toplevel.transition -> Toplevel.transition
    84 end;
    85 
    86 structure Isar_Cmd: ISAR_CMD =
    87 struct
    88 
    89 
    90 (** theory declarations **)
    91 
    92 (* generic setup *)
    93 
    94 fun global_setup (txt, pos) =
    95   ML_Lex.read pos txt
    96   |> ML_Context.expression pos "val setup: theory -> theory" "Context.map_theory setup"
    97   |> Context.theory_map;
    98 
    99 fun local_setup (txt, pos) =
   100   ML_Lex.read pos txt
   101   |> ML_Context.expression pos "val setup: local_theory -> local_theory" "Context.map_proof setup"
   102   |> Context.proof_map;
   103 
   104 
   105 (* translation functions *)
   106 
   107 local
   108 
   109 fun advancedT false = ""
   110   | advancedT true = "Proof.context -> ";
   111 
   112 fun advancedN false = ""
   113   | advancedN true = "advanced_";
   114 
   115 in
   116 
   117 fun parse_ast_translation (a, (txt, pos)) =
   118   ML_Lex.read pos txt
   119   |> ML_Context.expression pos
   120     ("val parse_ast_translation: (string * (" ^ advancedT a ^
   121       "Ast.ast list -> Ast.ast)) list")
   122     ("Context.map_theory (Sign.add_" ^ advancedN a ^ "trfuns (parse_ast_translation, [], [], []))")
   123   |> Context.theory_map;
   124 
   125 fun parse_translation (a, (txt, pos)) =
   126   ML_Lex.read pos txt
   127   |> ML_Context.expression pos
   128     ("val parse_translation: (string * (" ^ advancedT a ^
   129       "term list -> term)) list")
   130     ("Context.map_theory (Sign.add_" ^ advancedN a ^ "trfuns ([], parse_translation, [], []))")
   131   |> Context.theory_map;
   132 
   133 fun print_translation (a, (txt, pos)) =
   134   ML_Lex.read pos txt
   135   |> ML_Context.expression pos
   136     ("val print_translation: (string * (" ^ advancedT a ^
   137       "term list -> term)) list")
   138     ("Context.map_theory (Sign.add_" ^ advancedN a ^ "trfuns ([], [], print_translation, []))")
   139   |> Context.theory_map;
   140 
   141 fun print_ast_translation (a, (txt, pos)) =
   142   ML_Lex.read pos txt
   143   |> ML_Context.expression pos
   144     ("val print_ast_translation: (string * (" ^ advancedT a ^
   145       "Ast.ast list -> Ast.ast)) list")
   146     ("Context.map_theory (Sign.add_" ^ advancedN a ^ "trfuns ([], [], [], print_ast_translation))")
   147   |> Context.theory_map;
   148 
   149 fun typed_print_translation (a, (txt, pos)) =
   150   ML_Lex.read pos txt
   151   |> ML_Context.expression pos
   152     ("val typed_print_translation: (string * (" ^ advancedT a ^ "typ -> term list -> term)) list")
   153     ("Context.map_theory (Sign.add_" ^ advancedN a ^ "trfunsT typed_print_translation)")
   154   |> Context.theory_map;
   155 
   156 end;
   157 
   158 
   159 (* translation rules *)
   160 
   161 fun read_trrules thy raw_rules =
   162   let
   163     val ctxt = Proof_Context.init_global thy;
   164   in
   165     raw_rules |> map (Syntax.map_trrule (fn (r, s) =>
   166       Syntax_Phases.parse_ast_pattern ctxt (Proof_Context.intern_type ctxt r, s)))
   167   end;
   168 
   169 fun translations args thy = Sign.add_trrules (read_trrules thy args) thy;
   170 fun no_translations args thy = Sign.del_trrules (read_trrules thy args) thy;
   171 
   172 
   173 (* oracles *)
   174 
   175 fun oracle (name, pos) (body_txt, body_pos) =
   176   let
   177     val body = ML_Lex.read body_pos body_txt;
   178     val ants =
   179       ML_Lex.read Position.none
   180        ("local\n\
   181         \  val binding = " ^ ML_Syntax.make_binding (name, pos) ^ ";\n\
   182         \  val body = ") @ body @ ML_Lex.read Position.none (";\n\
   183         \in\n\
   184         \  val " ^ name ^ " = snd (Context.>>> (Context.map_theory_result (Thm.add_oracle (binding, body))));\n\
   185         \end;\n");
   186   in Context.theory_map (ML_Context.exec (fn () => ML_Context.eval false body_pos ants)) end;
   187 
   188 
   189 (* old-style axioms *)
   190 
   191 val add_axioms = fold (snd oo Specification.axiom_cmd);
   192 
   193 fun add_defs ((unchecked, overloaded), args) thy =
   194   thy |>
   195     (if unchecked then Global_Theory.add_defs_unchecked_cmd else Global_Theory.add_defs_cmd)
   196       overloaded
   197       (map (fn ((b, ax), srcs) => ((b, ax), map (Attrib.attribute_cmd_global thy) srcs)) args)
   198   |> snd;
   199 
   200 
   201 (* declarations *)
   202 
   203 fun declaration {syntax, pervasive} (txt, pos) =
   204   ML_Lex.read pos txt
   205   |> ML_Context.expression pos
   206     "val declaration: Morphism.declaration"
   207     ("Context.map_proof (Local_Theory.declaration {syntax = " ^ Bool.toString syntax ^ ", \
   208       \pervasive = " ^ Bool.toString pervasive ^ "} declaration)")
   209   |> Context.proof_map;
   210 
   211 
   212 (* simprocs *)
   213 
   214 fun simproc_setup name lhss (txt, pos) identifier =
   215   ML_Lex.read pos txt
   216   |> ML_Context.expression pos
   217     "val proc: Morphism.morphism -> Simplifier.simpset -> cterm -> thm option"
   218     ("Context.map_proof (Simplifier.def_simproc_cmd {name = " ^ ML_Syntax.make_binding name ^ ", \
   219       \lhss = " ^ ML_Syntax.print_strings lhss ^ ", proc = proc, \
   220       \identifier = Library.maps ML_Context.thms " ^ ML_Syntax.print_strings identifier ^ "})")
   221   |> Context.proof_map;
   222 
   223 
   224 (* hide names *)
   225 
   226 fun hide_names intern check hide fully xnames thy =
   227   let
   228     val names = map (intern thy) xnames;
   229     val bads = filter_out (check thy) names;
   230   in
   231     if null bads then fold (hide fully) names thy
   232     else error ("Attempt to hide undeclared item(s): " ^ commas_quote bads)
   233   end;
   234 
   235 val hide_class = hide_names Sign.intern_class (can o Sign.certify_class) Sign.hide_class;
   236 val hide_type = hide_names Sign.intern_type Sign.declared_tyname Sign.hide_type;
   237 val hide_const = hide_names Sign.intern_const Sign.declared_const Sign.hide_const;
   238 val hide_fact =
   239   hide_names Global_Theory.intern_fact Global_Theory.defined_fact Global_Theory.hide_fact;
   240 
   241 
   242 (* goals *)
   243 
   244 fun goal opt_chain goal stmt int =
   245   opt_chain #> goal NONE (K I) stmt int;
   246 
   247 val have = goal I Proof.have_cmd;
   248 val hence = goal Proof.chain Proof.have_cmd;
   249 val show = goal I Proof.show_cmd;
   250 val thus = goal Proof.chain Proof.show_cmd;
   251 
   252 
   253 (* local endings *)
   254 
   255 fun local_qed m = Toplevel.proof (Proof.local_qed (m, true));
   256 val local_terminal_proof = Toplevel.proof' o Proof.local_future_terminal_proof;
   257 val local_default_proof = Toplevel.proof Proof.local_default_proof;
   258 val local_immediate_proof = Toplevel.proof Proof.local_immediate_proof;
   259 val local_done_proof = Toplevel.proof Proof.local_done_proof;
   260 val local_skip_proof = Toplevel.proof' Proof.local_skip_proof;
   261 
   262 val skip_local_qed = Toplevel.skip_proof (fn i => if i > 1 then i - 1 else raise Toplevel.UNDEF);
   263 
   264 
   265 (* global endings *)
   266 
   267 fun global_qed m = Toplevel.end_proof (K (Proof.global_qed (m, true)));
   268 val global_terminal_proof = Toplevel.end_proof o K o Proof.global_terminal_proof;
   269 val global_default_proof = Toplevel.end_proof (K Proof.global_default_proof);
   270 val global_immediate_proof = Toplevel.end_proof (K Proof.global_immediate_proof);
   271 val global_skip_proof = Toplevel.end_proof Proof.global_skip_proof;
   272 val global_done_proof = Toplevel.end_proof (K Proof.global_done_proof);
   273 
   274 val skip_global_qed = Toplevel.skip_proof_to_theory (fn n => n = 1);
   275 
   276 
   277 (* common endings *)
   278 
   279 fun qed m = local_qed m o global_qed m o skip_local_qed o skip_global_qed;
   280 fun terminal_proof m = local_terminal_proof m o global_terminal_proof m;
   281 val default_proof = local_default_proof o global_default_proof;
   282 val immediate_proof = local_immediate_proof o global_immediate_proof;
   283 val done_proof = local_done_proof o global_done_proof;
   284 val skip_proof = local_skip_proof o global_skip_proof;
   285 
   286 
   287 (* diagnostic ML evaluation *)
   288 
   289 structure Diag_State = Proof_Data
   290 (
   291   type T = Toplevel.state;
   292   fun init _ = Toplevel.toplevel;
   293 );
   294 
   295 fun ml_diag verbose (txt, pos) = Toplevel.keep (fn state =>
   296   let val opt_ctxt =
   297     try Toplevel.generic_theory_of state
   298     |> Option.map (Context.proof_of #> Diag_State.put state)
   299   in ML_Context.eval_text_in opt_ctxt verbose pos txt end);
   300 
   301 val diag_state = Diag_State.get;
   302 
   303 fun diag_goal ctxt =
   304   Proof.goal (Toplevel.proof_of (diag_state ctxt))
   305     handle Toplevel.UNDEF => error "No goal present";
   306 
   307 val _ =
   308   Context.>> (Context.map_theory
   309    (ML_Antiquote.value (Binding.qualify true "Isar" (Binding.name "state"))
   310       (Scan.succeed "Isar_Cmd.diag_state ML_context") #>
   311     ML_Antiquote.value (Binding.qualify true "Isar" (Binding.name "goal"))
   312       (Scan.succeed "Isar_Cmd.diag_goal ML_context")));
   313 
   314 
   315 (* present draft files *)
   316 
   317 fun display_drafts names = Toplevel.imperative (fn () =>
   318   let
   319     val paths = map Path.explode names;
   320     val outfile = File.shell_path (Present.drafts (getenv "ISABELLE_DOC_FORMAT") paths);
   321   in Isabelle_System.isabelle_tool "display" ("-c " ^ outfile ^ " &"); () end);
   322 
   323 fun print_drafts names = Toplevel.imperative (fn () =>
   324   let
   325     val paths = map Path.explode names;
   326     val outfile = File.shell_path (Present.drafts "ps" paths);
   327   in Isabelle_System.isabelle_tool "print" ("-c " ^ outfile); () end);
   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 (Pretty.writeln o Proof_Display.pretty_full_theory verbose o Toplevel.theory_of);
   336 
   337 val print_syntax = Toplevel.unknown_context o
   338   Toplevel.keep (Proof_Context.print_syntax o Toplevel.context_of);
   339 
   340 val print_abbrevs = Toplevel.unknown_context o
   341   Toplevel.keep (Proof_Context.print_abbrevs o Toplevel.context_of);
   342 
   343 val print_facts = Toplevel.unknown_context o
   344   Toplevel.keep (Proof_Context.print_lthms o Toplevel.context_of);
   345 
   346 val print_configs = Toplevel.unknown_context o
   347   Toplevel.keep (Attrib.print_configs o Toplevel.context_of);
   348 
   349 val print_theorems_proof =
   350   Toplevel.keep (Proof_Context.print_lthms o Proof.context_of o Toplevel.proof_of);
   351 
   352 fun print_theorems_theory verbose = Toplevel.keep (fn state =>
   353   Toplevel.theory_of state |>
   354   (case Toplevel.previous_context_of state of
   355     SOME prev => Proof_Display.print_theorems_diff verbose (Proof_Context.theory_of prev)
   356   | NONE => Proof_Display.print_theorems verbose));
   357 
   358 fun print_theorems verbose =
   359   Toplevel.unknown_context o print_theorems_theory verbose o print_theorems_proof;
   360 
   361 val print_locales = Toplevel.unknown_theory o
   362   Toplevel.keep (Locale.print_locales o Toplevel.theory_of);
   363 
   364 fun print_locale (verbose, name) = Toplevel.unknown_theory o
   365   Toplevel.keep (fn state => Locale.print_locale (Toplevel.theory_of state) verbose name);
   366 
   367 fun print_registrations name = Toplevel.unknown_context o
   368   Toplevel.keep (fn state =>
   369     Locale.print_registrations (Toplevel.context_of state) name);
   370 
   371 fun print_dependencies (clean, expression) = Toplevel.unknown_context o
   372   Toplevel.keep (fn state =>
   373     Expression.print_dependencies (Toplevel.context_of state) clean expression);
   374 
   375 val print_attributes = Toplevel.unknown_theory o
   376   Toplevel.keep (Attrib.print_attributes o Toplevel.theory_of);
   377 
   378 val print_simpset = Toplevel.unknown_context o
   379   Toplevel.keep (fn state =>
   380     let val ctxt = Toplevel.context_of state
   381     in Pretty.writeln (Simplifier.pretty_ss ctxt (simpset_of ctxt)) end);
   382 
   383 val print_rules = Toplevel.unknown_context o
   384   Toplevel.keep (Context_Rules.print_rules o Toplevel.context_of);
   385 
   386 val print_trans_rules = Toplevel.unknown_context o
   387   Toplevel.keep (Calculation.print_rules o Toplevel.context_of);
   388 
   389 val print_methods = Toplevel.unknown_theory o
   390   Toplevel.keep (Method.print_methods o Toplevel.theory_of);
   391 
   392 val print_antiquotations =
   393   Toplevel.keep (Thy_Output.print_antiquotations o Toplevel.context_of);
   394 
   395 val thy_deps = Toplevel.unknown_theory o Toplevel.keep (fn state =>
   396   let
   397     val thy = Toplevel.theory_of state;
   398     val thy_session = Present.session_name thy;
   399 
   400     val gr = rev (Theory.nodes_of thy) |> map (fn node =>
   401       let
   402         val name = Context.theory_name node;
   403         val parents = map Context.theory_name (Theory.parents_of node);
   404         val session = Present.session_name node;
   405         val unfold = (session = thy_session);
   406       in {name = name, ID = name, parents = parents, dir = session, unfold = unfold, path = ""} end);
   407   in Present.display_graph gr end);
   408 
   409 val class_deps = Toplevel.unknown_theory o Toplevel.keep (fn state =>
   410   let
   411     val ctxt = Toplevel.context_of state;
   412     val {classes = (space, algebra), ...} = Type.rep_tsig (Proof_Context.tsig_of ctxt);
   413     val classes = Sorts.classes_of algebra;
   414     fun entry (c, (i, (_, cs))) =
   415       (i, {name = Name_Space.extern ctxt space c, ID = c, parents = Graph.Keys.dest cs,
   416             dir = "", unfold = true, path = ""});
   417     val gr =
   418       Graph.fold (cons o entry) classes []
   419       |> sort (int_ord o pairself #1) |> map #2;
   420   in Present.display_graph gr end);
   421 
   422 fun thm_deps args = Toplevel.unknown_theory o Toplevel.keep (fn state =>
   423   Thm_Deps.thm_deps (Toplevel.theory_of state)
   424     (Attrib.eval_thms (Toplevel.context_of state) args));
   425 
   426 
   427 (* find unused theorems *)
   428 
   429 fun unused_thms opt_range = Toplevel.keep (fn state =>
   430   let
   431     val thy = Toplevel.theory_of state;
   432     val ctxt = Toplevel.context_of state;
   433     fun pretty_thm (a, th) = Proof_Context.pretty_fact ctxt (a, [th]);
   434     val get_theory = Context.get_theory thy;
   435   in
   436     Thm_Deps.unused_thms
   437       (case opt_range of
   438         NONE => (Theory.parents_of thy, [thy])
   439       | SOME (xs, NONE) => (map get_theory xs, [thy])
   440       | SOME (xs, SOME ys) => (map get_theory xs, map get_theory ys))
   441     |> map pretty_thm |> Pretty.chunks |> Pretty.writeln
   442   end);
   443 
   444 
   445 (* print proof context contents *)
   446 
   447 val print_binds = Toplevel.unknown_context o
   448   Toplevel.keep (Proof_Context.print_binds o Toplevel.context_of);
   449 
   450 val print_cases = Toplevel.unknown_context o
   451   Toplevel.keep (Proof_Context.print_cases o Toplevel.context_of);
   452 
   453 
   454 (* print theorems, terms, types etc. *)
   455 
   456 local
   457 
   458 fun string_of_stmts ctxt args =
   459   Attrib.eval_thms ctxt args
   460   |> map (Element.pretty_statement ctxt Thm.theoremK)
   461   |> Pretty.chunks2 |> Pretty.string_of;
   462 
   463 fun string_of_thms ctxt args =
   464   Pretty.string_of (Display.pretty_thms ctxt (Attrib.eval_thms ctxt args));
   465 
   466 fun string_of_prfs full state arg =
   467   Pretty.string_of
   468     (case arg of
   469       NONE =>
   470         let
   471           val {context = ctxt, goal = thm} = Proof.simple_goal (Toplevel.proof_of state);
   472           val thy = Proof_Context.theory_of ctxt;
   473           val prf = Thm.proof_of thm;
   474           val prop = Thm.full_prop_of thm;
   475           val prf' = Proofterm.rewrite_proof_notypes ([], []) prf;
   476         in
   477           Proof_Syntax.pretty_proof ctxt
   478             (if full then Reconstruct.reconstruct_proof thy prop prf' else prf')
   479         end
   480     | SOME srcs =>
   481         let val ctxt = Toplevel.context_of state
   482         in map (Proof_Syntax.pretty_proof_of ctxt full) (Attrib.eval_thms ctxt srcs) end
   483         |> Pretty.chunks);
   484 
   485 fun string_of_prop ctxt s =
   486   let
   487     val prop = Syntax.read_prop ctxt s;
   488     val ctxt' = Variable.auto_fixes prop ctxt;
   489   in Pretty.string_of (Pretty.quote (Syntax.pretty_term ctxt' prop)) end;
   490 
   491 fun string_of_term ctxt s =
   492   let
   493     val t = Syntax.read_term ctxt s;
   494     val T = Term.type_of t;
   495     val ctxt' = Variable.auto_fixes t ctxt;
   496   in
   497     Pretty.string_of
   498       (Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t), Pretty.fbrk,
   499         Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' T)])
   500   end;
   501 
   502 fun string_of_type ctxt (s, NONE) =
   503       let val T = Syntax.read_typ ctxt s
   504       in Pretty.string_of (Pretty.quote (Syntax.pretty_typ ctxt T)) end
   505   | string_of_type ctxt (s1, SOME s2) =
   506       let
   507         val ctxt' = Config.put show_sorts true ctxt;
   508         val raw_T = Syntax.parse_typ ctxt' s1;
   509         val S = Syntax.read_sort ctxt' s2;
   510         val T =
   511           Syntax.check_term ctxt'
   512             (Logic.mk_type raw_T |> Type.constraint (Term.itselfT (Type_Infer.anyT S)))
   513           |> Logic.dest_type;
   514       in Pretty.string_of (Pretty.quote (Syntax.pretty_typ ctxt' T)) end;
   515 
   516 fun print_item string_of (modes, arg) = Toplevel.keep (fn state =>
   517   Print_Mode.with_modes modes (fn () => writeln (string_of state arg)) ());
   518 
   519 in
   520 
   521 val print_stmts = print_item (string_of_stmts o Toplevel.context_of);
   522 val print_thms = print_item (string_of_thms o Toplevel.context_of);
   523 val print_prfs = print_item o string_of_prfs;
   524 val print_prop = print_item (string_of_prop o Toplevel.context_of);
   525 val print_term = print_item (string_of_term o Toplevel.context_of);
   526 val print_type = print_item (string_of_type o Toplevel.context_of);
   527 
   528 end;
   529 
   530 
   531 (* markup commands *)
   532 
   533 fun header_markup txt = Toplevel.keep (fn state =>
   534   if Toplevel.is_toplevel state then Thy_Output.check_text txt state
   535   else raise Toplevel.UNDEF);
   536 
   537 fun local_theory_markup (loc, txt) = Toplevel.present_local_theory loc (Thy_Output.check_text txt);
   538 val proof_markup = Toplevel.present_proof o Thy_Output.check_text;
   539 
   540 end;