src/Pure/Thy/thy_output.ML
author wenzelm
Thu Nov 02 10:16:22 2017 +0100 (19 months ago)
changeset 66987 352b23c97ac8
parent 66021 08ab52fb9db5
child 67138 82283d52b4d6
permissions -rw-r--r--
support focus_session, for much faster startup of Isabelle/jEdit;
more options for "isabelle jedit";
     1 (*  Title:      Pure/Thy/thy_output.ML
     2     Author:     Markus Wenzel, TU Muenchen
     3 
     4 Theory document output with antiquotations.
     5 *)
     6 
     7 signature THY_OUTPUT =
     8 sig
     9   val display: bool Config.T
    10   val quotes: bool Config.T
    11   val margin: int Config.T
    12   val indent: int Config.T
    13   val source: bool Config.T
    14   val break: bool Config.T
    15   val modes: string Config.T
    16   val add_wrapper: ((unit -> string) -> unit -> string) -> Proof.context -> Proof.context
    17   val add_option: binding -> (string -> Proof.context -> Proof.context) -> theory -> theory
    18   val check_command: Proof.context -> xstring * Position.T -> string
    19   val check_option: Proof.context -> xstring * Position.T -> string
    20   val print_antiquotations: bool -> Proof.context -> unit
    21   val antiquotation: binding -> 'a context_parser ->
    22     ({source: Token.src, state: Toplevel.state, context: Proof.context} -> 'a -> string) ->
    23       theory -> theory
    24   val boolean: string -> bool
    25   val integer: string -> int
    26   val eval_antiquote: Toplevel.state -> Antiquote.text_antiquote -> string
    27   val output_text: Toplevel.state -> {markdown: bool} -> Input.source -> string
    28   val present_thy: theory -> (Toplevel.transition * Toplevel.state) list -> Token.T list -> Buffer.T
    29   val pretty_text: Proof.context -> string -> Pretty.T
    30   val pretty_term: Proof.context -> term -> Pretty.T
    31   val pretty_thm: Proof.context -> thm -> Pretty.T
    32   val str_of_source: Token.src -> string
    33   val maybe_pretty_source: (Proof.context -> 'a -> Pretty.T) -> Proof.context ->
    34     Token.src -> 'a list -> Pretty.T list
    35   val string_of_margin: Proof.context -> Pretty.T -> string
    36   val output: Proof.context -> Pretty.T list -> string
    37   val verbatim_text: Proof.context -> string -> string
    38   val document_command: {markdown: bool} -> (xstring * Position.T) option * Input.source ->
    39     Toplevel.transition -> Toplevel.transition
    40 end;
    41 
    42 structure Thy_Output: THY_OUTPUT =
    43 struct
    44 
    45 (** options **)
    46 
    47 val display = Attrib.setup_option_bool ("thy_output_display", \<^here>);
    48 val break = Attrib.setup_option_bool ("thy_output_break", \<^here>);
    49 val quotes = Attrib.setup_option_bool ("thy_output_quotes", \<^here>);
    50 val margin = Attrib.setup_option_int ("thy_output_margin", \<^here>);
    51 val indent = Attrib.setup_option_int ("thy_output_indent", \<^here>);
    52 val source = Attrib.setup_option_bool ("thy_output_source", \<^here>);
    53 val modes = Attrib.setup_option_string ("thy_output_modes", \<^here>);
    54 
    55 
    56 structure Wrappers = Proof_Data
    57 (
    58   type T = ((unit -> string) -> unit -> string) list;
    59   fun init _ = [];
    60 );
    61 
    62 fun add_wrapper wrapper = Wrappers.map (cons wrapper);
    63 
    64 val wrap = Wrappers.get #> fold (fn wrapper => fn f => wrapper f);
    65 
    66 
    67 
    68 (** maintain global antiquotations **)
    69 
    70 structure Antiquotations = Theory_Data
    71 (
    72   type T =
    73     (Token.src -> Toplevel.state -> Proof.context -> string) Name_Space.table *
    74       (string -> Proof.context -> Proof.context) Name_Space.table;
    75   val empty : T =
    76     (Name_Space.empty_table Markup.document_antiquotationN,
    77       Name_Space.empty_table Markup.document_antiquotation_optionN);
    78   val extend = I;
    79   fun merge ((commands1, options1), (commands2, options2)) : T =
    80     (Name_Space.merge_tables (commands1, commands2),
    81       Name_Space.merge_tables (options1, options2));
    82 );
    83 
    84 val get_antiquotations = Antiquotations.get o Proof_Context.theory_of;
    85 
    86 fun add_command name cmd thy = thy
    87   |> Antiquotations.map (apfst (Name_Space.define (Context.Theory thy) true (name, cmd) #> snd));
    88 
    89 fun add_option name opt thy = thy
    90   |> Antiquotations.map (apsnd (Name_Space.define (Context.Theory thy) true (name, opt) #> snd));
    91 
    92 fun check_command ctxt = #1 o Name_Space.check (Context.Proof ctxt) (#1 (get_antiquotations ctxt));
    93 
    94 fun check_option ctxt = #1 o Name_Space.check (Context.Proof ctxt) (#2 (get_antiquotations ctxt));
    95 
    96 fun command src state ctxt =
    97   let val (src', f) = Token.check_src ctxt (#1 o get_antiquotations) src
    98   in f src' state ctxt end;
    99 
   100 fun option ((xname, pos), s) ctxt =
   101   let
   102     val (_, opt) =
   103       Name_Space.check (Context.Proof ctxt) (#2 (get_antiquotations ctxt)) (xname, pos);
   104   in opt s ctxt end;
   105 
   106 fun print_antiquotations verbose ctxt =
   107   let
   108     val (commands, options) = get_antiquotations ctxt;
   109     val command_names = map #1 (Name_Space.markup_table verbose ctxt commands);
   110     val option_names = map #1 (Name_Space.markup_table verbose ctxt options);
   111   in
   112     [Pretty.big_list "document antiquotations:" (map Pretty.mark_str command_names),
   113      Pretty.big_list "document antiquotation options:" (map Pretty.mark_str option_names)]
   114   end |> Pretty.writeln_chunks;
   115 
   116 fun antiquotation name scan body =
   117   add_command name
   118     (fn src => fn state => fn ctxt =>
   119       let val (x, ctxt') = Token.syntax scan src ctxt
   120       in body {source = src, state = state, context = ctxt'} x end);
   121 
   122 
   123 
   124 (** syntax of antiquotations **)
   125 
   126 (* option values *)
   127 
   128 fun boolean "" = true
   129   | boolean "true" = true
   130   | boolean "false" = false
   131   | boolean s = error ("Bad boolean value: " ^ quote s);
   132 
   133 fun integer s =
   134   let
   135     fun int ss =
   136       (case Library.read_int ss of (i, []) => i
   137       | _ => error ("Bad integer value: " ^ quote s));
   138   in (case Symbol.explode s of "-" :: ss => ~ (int ss) | ss => int ss) end;
   139 
   140 
   141 (* outer syntax *)
   142 
   143 local
   144 
   145 val property =
   146   Parse.position Parse.name -- Scan.optional (Parse.$$$ "=" |-- Parse.!!! Parse.name) "";
   147 
   148 val properties =
   149   Scan.optional (Parse.$$$ "[" |-- Parse.!!! (Parse.enum "," property --| Parse.$$$ "]")) [];
   150 
   151 in
   152 
   153 val antiq =
   154   Parse.!!!
   155     (Parse.token Parse.liberal_name -- properties -- Parse.args --| Scan.ahead Parse.eof)
   156   >> (fn ((name, props), args) => (props, name :: args));
   157 
   158 end;
   159 
   160 
   161 (* eval antiquote *)
   162 
   163 local
   164 
   165 fun eval_antiq state (opts, src) =
   166   let
   167     val preview_ctxt = fold option opts (Toplevel.presentation_context_of state);
   168     val print_ctxt = Context_Position.set_visible false preview_ctxt;
   169 
   170     fun cmd ctxt = wrap ctxt (fn () => command src state ctxt) ();
   171     val _ = cmd preview_ctxt;
   172     val print_modes = space_explode "," (Config.get print_ctxt modes) @ [Latex.latexN];
   173   in Print_Mode.with_modes print_modes (fn () => cmd print_ctxt) () end;
   174 
   175 in
   176 
   177 fun eval_antiquote _ (Antiquote.Text ss) = Symbol_Pos.content ss
   178   | eval_antiquote state (Antiquote.Control {name, body, ...}) =
   179       eval_antiq state
   180         ([], Token.make_src name (if null body then [] else [Token.read_cartouche body]))
   181   | eval_antiquote state (Antiquote.Antiq {range = (pos, _), body, ...}) =
   182       let
   183         val keywords =
   184           (case try Toplevel.presentation_context_of state of
   185             SOME ctxt => Thy_Header.get_keywords' ctxt
   186           | NONE =>
   187               error ("Unknown context -- cannot expand document antiquotations" ^
   188                 Position.here pos));
   189       in eval_antiq state (Token.read_antiq keywords antiq (body, pos)) end;
   190 
   191 end;
   192 
   193 
   194 (* output text *)
   195 
   196 fun output_text state {markdown} source =
   197   let
   198     val is_reported =
   199       (case try Toplevel.context_of state of
   200         SOME ctxt => Context_Position.is_visible ctxt
   201       | NONE => true);
   202 
   203     val pos = Input.pos_of source;
   204     val syms = Input.source_explode source;
   205 
   206     val _ =
   207       if is_reported then
   208         Position.report pos (Markup.language_document (Input.is_delimited source))
   209       else ();
   210 
   211     val output_antiquotes = map (eval_antiquote state) #> implode;
   212 
   213     fun output_line line =
   214       (if Markdown.line_is_item line then "\\item " else "") ^
   215         output_antiquotes (Markdown.line_content line);
   216 
   217     fun output_blocks blocks = space_implode "\n\n" (map output_block blocks)
   218     and output_block (Markdown.Par lines) = cat_lines (map output_line lines)
   219       | output_block (Markdown.List {kind, body, ...}) =
   220           Latex.environment (Markdown.print_kind kind) (output_blocks body);
   221   in
   222     if Toplevel.is_skipped_proof state then ""
   223     else if markdown andalso exists (Markdown.is_control o Symbol_Pos.symbol) syms
   224     then
   225       let
   226         val ants = Antiquote.parse pos syms;
   227         val reports = Antiquote.antiq_reports ants;
   228         val blocks = Markdown.read_antiquotes ants;
   229         val _ = if is_reported then Position.reports (reports @ Markdown.reports blocks) else ();
   230       in output_blocks blocks end
   231     else
   232       let
   233         val ants = Antiquote.parse pos (Symbol_Pos.trim_blanks syms);
   234         val reports = Antiquote.antiq_reports ants;
   235         val _ = if is_reported then Position.reports (reports @ Markdown.text_reports ants) else ();
   236       in output_antiquotes ants end
   237   end;
   238 
   239 
   240 
   241 (** present theory source **)
   242 
   243 (*NB: arranging white space around command spans is a black art*)
   244 
   245 (* presentation tokens *)
   246 
   247 datatype token =
   248     No_Token
   249   | Basic_Token of Token.T
   250   | Markup_Token of string * Input.source
   251   | Markup_Env_Token of string * Input.source
   252   | Raw_Token of Input.source;
   253 
   254 fun basic_token pred (Basic_Token tok) = pred tok
   255   | basic_token _ _ = false;
   256 
   257 val improper_token = basic_token Token.is_improper;
   258 val comment_token = basic_token Token.is_comment;
   259 val blank_token = basic_token Token.is_blank;
   260 val newline_token = basic_token Token.is_newline;
   261 
   262 
   263 (* output token *)
   264 
   265 fun output_token state tok =
   266   (case tok of
   267     No_Token => ""
   268   | Basic_Token tok => Latex.output_token tok
   269   | Markup_Token (cmd, source) =>
   270       "%\n\\isamarkup" ^ cmd ^ "{" ^ output_text state {markdown = false} source ^ "%\n}\n"
   271   | Markup_Env_Token (cmd, source) =>
   272       Latex.environment ("isamarkup" ^ cmd) (output_text state {markdown = true} source)
   273   | Raw_Token source =>
   274       "%\n" ^ output_text state {markdown = true} source ^ "\n");
   275 
   276 
   277 (* command spans *)
   278 
   279 type command = string * Position.T * string list;   (*name, position, tags*)
   280 type source = (token * (string * int)) list;        (*token, markup flag, meta-comment depth*)
   281 
   282 datatype span = Span of command * (source * source * source * source) * bool;
   283 
   284 fun make_span cmd src =
   285   let
   286     fun take_newline (tok :: toks) =
   287           if newline_token (fst tok) then ([tok], toks, true)
   288           else ([], tok :: toks, false)
   289       | take_newline [] = ([], [], false);
   290     val (((src_prefix, src_main), src_suffix1), (src_suffix2, src_appendix, newline)) =
   291       src
   292       |> take_prefix (improper_token o fst)
   293       ||>> take_suffix (improper_token o fst)
   294       ||>> take_prefix (comment_token o fst)
   295       ||> take_newline;
   296   in Span (cmd, (src_prefix, src_main, src_suffix1 @ src_suffix2, src_appendix), newline) end;
   297 
   298 
   299 (* present spans *)
   300 
   301 local
   302 
   303 fun err_bad_nesting pos =
   304   error ("Bad nesting of commands in presentation" ^ pos);
   305 
   306 fun edge which f (x: string option, y) =
   307   if x = y then I
   308   else (case which (x, y) of NONE => I | SOME txt => Buffer.add (f txt));
   309 
   310 val begin_tag = edge #2 Latex.begin_tag;
   311 val end_tag = edge #1 Latex.end_tag;
   312 fun open_delim delim e = edge #2 Latex.begin_delim e #> delim #> edge #2 Latex.end_delim e;
   313 fun close_delim delim e = edge #1 Latex.begin_delim e #> delim #> edge #1 Latex.end_delim e;
   314 
   315 in
   316 
   317 fun present_span keywords span state state' (tag_stack, active_tag, newline, buffer, present_cont) =
   318   let
   319     val present = fold (fn (tok, (flag, 0)) =>
   320         Buffer.add (output_token state' tok)
   321         #> Buffer.add flag
   322       | _ => I);
   323 
   324     val Span ((cmd_name, cmd_pos, cmd_tags), srcs, span_newline) = span;
   325 
   326     val (tag, tags) = tag_stack;
   327     val tag' = try hd (fold (update (op =)) cmd_tags (the_list tag));
   328 
   329     val nesting = Toplevel.level state' - Toplevel.level state;
   330 
   331     val active_tag' =
   332       if is_some tag' then tag'
   333       else if cmd_name = "end" andalso not (Toplevel.is_toplevel state') then NONE
   334       else
   335         (case Keyword.command_tags keywords cmd_name of
   336           default_tag :: _ => SOME default_tag
   337         | [] =>
   338             if Keyword.is_vacuous keywords cmd_name andalso Toplevel.is_proof state
   339             then active_tag
   340             else NONE);
   341 
   342     val edge = (active_tag, active_tag');
   343 
   344     val newline' =
   345       if is_none active_tag' then span_newline else newline;
   346 
   347     val tag_stack' =
   348       if nesting = 0 andalso not (Toplevel.is_proof state) then tag_stack
   349       else if nesting >= 0 then (tag', replicate nesting tag @ tags)
   350       else
   351         (case drop (~ nesting - 1) tags of
   352           tg :: tgs => (tg, tgs)
   353         | [] => err_bad_nesting (Position.here cmd_pos));
   354 
   355     val buffer' =
   356       buffer
   357       |> end_tag edge
   358       |> close_delim (fst present_cont) edge
   359       |> snd present_cont
   360       |> open_delim (present (#1 srcs)) edge
   361       |> begin_tag edge
   362       |> present (#2 srcs);
   363     val present_cont' =
   364       if newline then (present (#3 srcs), present (#4 srcs))
   365       else (I, present (#3 srcs) #> present (#4 srcs));
   366   in (tag_stack', active_tag', newline', buffer', present_cont') end;
   367 
   368 fun present_trailer ((_, tags), active_tag, _, buffer, present_cont) =
   369   if not (null tags) then err_bad_nesting " at end of theory"
   370   else
   371     buffer
   372     |> end_tag (active_tag, NONE)
   373     |> close_delim (fst present_cont) (active_tag, NONE)
   374     |> snd present_cont;
   375 
   376 end;
   377 
   378 
   379 (* present_thy *)
   380 
   381 local
   382 
   383 val markup_true = "\\isamarkuptrue%\n";
   384 val markup_false = "\\isamarkupfalse%\n";
   385 
   386 val space_proper =
   387   Scan.one Token.is_blank -- Scan.many Token.is_comment -- Scan.one Token.is_proper;
   388 
   389 val is_improper = not o (Token.is_proper orf Token.is_begin_ignore orf Token.is_end_ignore);
   390 val improper = Scan.many is_improper;
   391 val improper_end = Scan.repeat (Scan.unless space_proper (Scan.one is_improper));
   392 val blank_end = Scan.repeat (Scan.unless space_proper (Scan.one Token.is_blank));
   393 
   394 val opt_newline = Scan.option (Scan.one Token.is_newline);
   395 
   396 val ignore =
   397   Scan.depend (fn d => opt_newline |-- Scan.one Token.is_begin_ignore
   398     >> pair (d + 1)) ||
   399   Scan.depend (fn d => Scan.one Token.is_end_ignore --|
   400     (if d = 0 then Scan.fail_with (K (fn () => "Bad nesting of meta-comments")) else opt_newline)
   401     >> pair (d - 1));
   402 
   403 val tag = (improper -- Parse.$$$ "%" -- improper) |-- Parse.!!! (Parse.tag_name --| blank_end);
   404 
   405 val locale =
   406   Scan.option ((Parse.$$$ "(" -- improper -- Parse.$$$ "in") |--
   407     Parse.!!! (improper |-- Parse.name --| (improper -- Parse.$$$ ")")));
   408 
   409 in
   410 
   411 fun present_thy thy command_results toks =
   412   let
   413     val keywords = Thy_Header.get_keywords thy;
   414 
   415 
   416     (* tokens *)
   417 
   418     val ignored = Scan.state --| ignore
   419       >> (fn d => (NONE, (No_Token, ("", d))));
   420 
   421     fun markup pred mk flag = Scan.peek (fn d =>
   422       improper |--
   423         Parse.position (Scan.one (fn tok =>
   424           Token.is_command tok andalso pred keywords (Token.content_of tok))) --
   425       Scan.repeat tag --
   426       Parse.!!!! ((improper -- locale -- improper) |-- Parse.document_source --| improper_end)
   427       >> (fn (((tok, pos'), tags), source) =>
   428         let val name = Token.content_of tok
   429         in (SOME (name, pos', tags), (mk (name, source), (flag, d))) end));
   430 
   431     val command = Scan.peek (fn d =>
   432       Scan.optional (Scan.one Token.is_command_modifier ::: improper) [] --
   433       Scan.one Token.is_command -- Scan.repeat tag
   434       >> (fn ((cmd_mod, cmd), tags) =>
   435         map (fn tok => (NONE, (Basic_Token tok, ("", d)))) cmd_mod @
   436           [(SOME (Token.content_of cmd, Token.pos_of cmd, tags),
   437             (Basic_Token cmd, (markup_false, d)))]));
   438 
   439     val cmt = Scan.peek (fn d =>
   440       (Parse.$$$ "--" || Parse.$$$ Symbol.comment) |--
   441         Parse.!!!! (improper |-- Parse.document_source) >>
   442         (fn source => (NONE, (Markup_Token ("cmt", source), ("", d)))));
   443 
   444     val other = Scan.peek (fn d =>
   445        Parse.not_eof >> (fn tok => (NONE, (Basic_Token tok, ("", d)))));
   446 
   447     val tokens =
   448       (ignored ||
   449         markup Keyword.is_document_heading Markup_Token markup_true ||
   450         markup Keyword.is_document_body Markup_Env_Token markup_true ||
   451         markup Keyword.is_document_raw (Raw_Token o #2) "") >> single ||
   452       command ||
   453       (cmt || other) >> single;
   454 
   455 
   456     (* spans *)
   457 
   458     val is_eof = fn (_, (Basic_Token x, _)) => Token.is_eof x | _ => false;
   459     val stopper = Scan.stopper (K (NONE, (Basic_Token Token.eof, ("", 0)))) is_eof;
   460 
   461     val cmd = Scan.one (is_some o fst);
   462     val non_cmd = Scan.one (is_none o fst andf not o is_eof) >> #2;
   463 
   464     val comments = Scan.many (comment_token o fst o snd);
   465     val blank = Scan.one (blank_token o fst o snd);
   466     val newline = Scan.one (newline_token o fst o snd);
   467     val before_cmd =
   468       Scan.option (newline -- comments) --
   469       Scan.option (newline -- comments) --
   470       Scan.option (blank -- comments) -- cmd;
   471 
   472     val span =
   473       Scan.repeat non_cmd -- cmd --
   474         Scan.repeat (Scan.unless before_cmd non_cmd) --
   475         Scan.option (newline >> (single o snd))
   476       >> (fn (((toks1, (cmd, tok2)), toks3), tok4) =>
   477           make_span (the cmd) (toks1 @ (tok2 :: (toks3 @ the_default [] tok4))));
   478 
   479     val spans = toks
   480       |> take_suffix Token.is_space |> #1
   481       |> Source.of_list
   482       |> Source.source' 0 Token.stopper (Scan.error (Scan.bulk tokens >> flat))
   483       |> Source.source stopper (Scan.error (Scan.bulk span))
   484       |> Source.exhaust;
   485 
   486 
   487     (* present commands *)
   488 
   489     fun present_command tr span st st' =
   490       Toplevel.setmp_thread_position tr (present_span keywords span st st');
   491 
   492     fun present _ [] = I
   493       | present st (((tr, st'), span) :: rest) = present_command tr span st st' #> present st' rest;
   494   in
   495     if length command_results = length spans then
   496       ((NONE, []), NONE, true, Buffer.empty, (I, I))
   497       |> present Toplevel.toplevel (command_results ~~ spans)
   498       |> present_trailer
   499     else error "Messed-up outer syntax for presentation"
   500   end;
   501 
   502 end;
   503 
   504 
   505 
   506 (** setup default output **)
   507 
   508 (* options *)
   509 
   510 val _ = Theory.setup
   511  (add_option @{binding show_types} (Config.put show_types o boolean) #>
   512   add_option @{binding show_sorts} (Config.put show_sorts o boolean) #>
   513   add_option @{binding show_structs} (Config.put show_structs o boolean) #>
   514   add_option @{binding show_question_marks} (Config.put show_question_marks o boolean) #>
   515   add_option @{binding show_abbrevs} (Config.put show_abbrevs o boolean) #>
   516   add_option @{binding names_long} (Config.put Name_Space.names_long o boolean) #>
   517   add_option @{binding names_short} (Config.put Name_Space.names_short o boolean) #>
   518   add_option @{binding names_unique} (Config.put Name_Space.names_unique o boolean) #>
   519   add_option @{binding eta_contract} (Config.put Syntax_Trans.eta_contract o boolean) #>
   520   add_option @{binding display} (Config.put display o boolean) #>
   521   add_option @{binding break} (Config.put break o boolean) #>
   522   add_option @{binding quotes} (Config.put quotes o boolean) #>
   523   add_option @{binding mode} (add_wrapper o Print_Mode.with_modes o single) #>
   524   add_option @{binding margin} (Config.put margin o integer) #>
   525   add_option @{binding indent} (Config.put indent o integer) #>
   526   add_option @{binding source} (Config.put source o boolean) #>
   527   add_option @{binding goals_limit} (Config.put Goal_Display.goals_limit o integer));
   528 
   529 
   530 (* basic pretty printing *)
   531 
   532 fun perhaps_trim ctxt =
   533   not (Config.get ctxt display) ? Symbol.trim_blanks;
   534 
   535 fun pretty_text ctxt =
   536   Pretty.chunks o map Pretty.str o map (perhaps_trim ctxt) o split_lines;
   537 
   538 fun pretty_term ctxt t = Syntax.pretty_term (Variable.auto_fixes t ctxt) t;
   539 
   540 fun pretty_thm ctxt = pretty_term ctxt o Thm.full_prop_of;
   541 
   542 fun pretty_term_style ctxt (style, t) =
   543   pretty_term ctxt (style t);
   544 
   545 fun pretty_thm_style ctxt (style, th) =
   546   pretty_term ctxt (style (Thm.full_prop_of th));
   547 
   548 fun pretty_term_typ ctxt (style, t) =
   549   let val t' = style t
   550   in pretty_term ctxt (Type.constraint (Term.fastype_of t') t') end;
   551 
   552 fun pretty_term_typeof ctxt (style, t) =
   553   Syntax.pretty_typ ctxt (Term.fastype_of (style t));
   554 
   555 fun pretty_const ctxt c =
   556   let
   557     val t = Const (c, Consts.type_scheme (Proof_Context.consts_of ctxt) c)
   558       handle TYPE (msg, _, _) => error msg;
   559     val ([t'], _) = Variable.import_terms true [t] ctxt;
   560   in pretty_term ctxt t' end;
   561 
   562 fun pretty_abbrev ctxt s =
   563   let
   564     val t = Syntax.read_term (Proof_Context.set_mode Proof_Context.mode_abbrev ctxt) s;
   565     fun err () = error ("Abbreviated constant expected: " ^ Syntax.string_of_term ctxt t);
   566     val (head, args) = Term.strip_comb t;
   567     val (c, T) = Term.dest_Const head handle TERM _ => err ();
   568     val (U, u) = Consts.the_abbreviation (Proof_Context.consts_of ctxt) c
   569       handle TYPE _ => err ();
   570     val t' = Term.betapplys (Envir.expand_atom T (U, u), args);
   571     val eq = Logic.mk_equals (t, t');
   572     val ctxt' = Variable.auto_fixes eq ctxt;
   573   in Proof_Context.pretty_term_abbrev ctxt' eq end;
   574 
   575 fun pretty_locale ctxt (name, pos) =
   576   let
   577     val thy = Proof_Context.theory_of ctxt
   578   in (Pretty.str o Locale.extern thy o Locale.check thy) (name, pos) end;
   579 
   580 fun pretty_class ctxt =
   581   Pretty.str o Proof_Context.extern_class ctxt o Proof_Context.read_class ctxt;
   582 
   583 fun pretty_type ctxt s =
   584   let val Type (name, _) = Proof_Context.read_type_name {proper = true, strict = false} ctxt s
   585   in Pretty.str (Proof_Context.extern_type ctxt name) end;
   586 
   587 fun pretty_prf full ctxt = Proof_Syntax.pretty_clean_proof_of ctxt full;
   588 
   589 fun pretty_theory ctxt (name, pos) = (Theory.check ctxt (name, pos); Pretty.str name);
   590 
   591 
   592 (* default output *)
   593 
   594 val str_of_source = space_implode " " o map Token.unparse o Token.args_of_src;
   595 
   596 fun maybe_pretty_source pretty ctxt src xs =
   597   map (pretty ctxt) xs  (*always pretty in order to exhibit errors!*)
   598   |> (if Config.get ctxt source then K [pretty_text ctxt (str_of_source src)] else I);
   599 
   600 fun string_of_margin ctxt = Pretty.string_of_margin (Config.get ctxt margin);
   601 
   602 fun output ctxt prts =
   603   prts
   604   |> Config.get ctxt quotes ? map Pretty.quote
   605   |> (if Config.get ctxt display then
   606         map (Pretty.indent (Config.get ctxt indent) #> string_of_margin ctxt #> Output.output)
   607         #> space_implode "\\isasep\\isanewline%\n"
   608         #> Latex.environment "isabelle"
   609       else
   610         map
   611           ((if Config.get ctxt break then string_of_margin ctxt else Pretty.unformatted_string_of)
   612             #> Output.output)
   613         #> space_implode "\\isasep\\isanewline%\n"
   614         #> enclose "\\isa{" "}");
   615 
   616 
   617 (* verbatim text *)
   618 
   619 fun verbatim_text ctxt =
   620   if Config.get ctxt display then
   621     split_lines #> map (prefix (Symbol.spaces (Config.get ctxt indent))) #> cat_lines #>
   622     Latex.output_ascii #> Latex.environment "isabellett"
   623   else
   624     split_lines #>
   625     map (Latex.output_ascii #> enclose "\\isatt{" "}") #>
   626     space_implode "\\isasep\\isanewline%\n";
   627 
   628 
   629 (* antiquotations for basic entities *)
   630 
   631 local
   632 
   633 fun basic_entities name scan pretty =
   634   antiquotation name scan (fn {source, context = ctxt, ...} =>
   635     output ctxt o maybe_pretty_source pretty ctxt source);
   636 
   637 fun basic_entities_style name scan pretty =
   638   antiquotation name scan (fn {source, context = ctxt, ...} => fn (style, xs) =>
   639     output ctxt
   640       (maybe_pretty_source (fn ctxt => fn x => pretty ctxt (style, x)) ctxt source xs));
   641 
   642 fun basic_entity name scan = basic_entities name (scan >> single);
   643 
   644 in
   645 
   646 val _ = Theory.setup
   647  (basic_entities_style @{binding thm} (Term_Style.parse -- Attrib.thms) pretty_thm_style #>
   648   basic_entity @{binding prop} (Term_Style.parse -- Args.prop) pretty_term_style #>
   649   basic_entity @{binding term} (Term_Style.parse -- Args.term) pretty_term_style #>
   650   basic_entity @{binding term_type} (Term_Style.parse -- Args.term) pretty_term_typ #>
   651   basic_entity @{binding typeof} (Term_Style.parse -- Args.term) pretty_term_typeof #>
   652   basic_entity @{binding const} (Args.const {proper = true, strict = false}) pretty_const #>
   653   basic_entity @{binding abbrev} (Scan.lift Args.embedded_inner_syntax) pretty_abbrev #>
   654   basic_entity @{binding typ} Args.typ_abbrev Syntax.pretty_typ #>
   655   basic_entity @{binding locale} (Scan.lift (Parse.position Args.name)) pretty_locale #>
   656   basic_entity @{binding class} (Scan.lift Args.embedded_inner_syntax) pretty_class #>
   657   basic_entity @{binding type} (Scan.lift Args.embedded) pretty_type #>
   658   basic_entities @{binding prf} Attrib.thms (pretty_prf false) #>
   659   basic_entities @{binding full_prf} Attrib.thms (pretty_prf true) #>
   660   basic_entity @{binding theory} (Scan.lift (Parse.position Args.name)) pretty_theory);
   661 
   662 end;
   663 
   664 
   665 
   666 (** document command **)
   667 
   668 fun document_command markdown (loc, txt) =
   669   Toplevel.keep (fn state =>
   670     (case loc of
   671       NONE => ignore (output_text state markdown txt)
   672     | SOME (_, pos) =>
   673         error ("Illegal target specification -- not a theory context" ^ Position.here pos))) o
   674   Toplevel.present_local_theory loc (fn state => ignore (output_text state markdown txt));
   675 
   676 end;