src/Pure/Thy/thy_output.ML
author wenzelm
Fri, 24 Aug 2012 12:35:39 +0200
changeset 48918 6e5fd4585512
parent 47005 421760a1efe7
child 48927 ef462b5558eb
permissions -rw-r--r--
check side-comments of command spans (normally filtered out in Outer_Syntax.toplevel_source);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/Thy/thy_output.ML
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
     2
    Author:     Markus Wenzel, TU Muenchen
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
     3
30390
ad591ee76c78 simplified interface to define document antiquotations, cf. antiquotatation, maybe_pretty_source, output;
wenzelm
parents: 30381
diff changeset
     4
Theory document output with antiquotations.
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
     5
*)
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
     6
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
     7
signature THY_OUTPUT =
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
     8
sig
38767
d8da44a8dd25 proper context for various Thy_Output options, via official configuration options in ML and Isar;
wenzelm
parents: 38766
diff changeset
     9
  val display_default: bool Unsynchronized.ref
d8da44a8dd25 proper context for various Thy_Output options, via official configuration options in ML and Isar;
wenzelm
parents: 38766
diff changeset
    10
  val quotes_default: bool Unsynchronized.ref
d8da44a8dd25 proper context for various Thy_Output options, via official configuration options in ML and Isar;
wenzelm
parents: 38766
diff changeset
    11
  val indent_default: int Unsynchronized.ref
d8da44a8dd25 proper context for various Thy_Output options, via official configuration options in ML and Isar;
wenzelm
parents: 38766
diff changeset
    12
  val source_default: bool Unsynchronized.ref
d8da44a8dd25 proper context for various Thy_Output options, via official configuration options in ML and Isar;
wenzelm
parents: 38766
diff changeset
    13
  val break_default: bool Unsynchronized.ref
d8da44a8dd25 proper context for various Thy_Output options, via official configuration options in ML and Isar;
wenzelm
parents: 38766
diff changeset
    14
  val display: bool Config.T
d8da44a8dd25 proper context for various Thy_Output options, via official configuration options in ML and Isar;
wenzelm
parents: 38766
diff changeset
    15
  val quotes: bool Config.T
d8da44a8dd25 proper context for various Thy_Output options, via official configuration options in ML and Isar;
wenzelm
parents: 38766
diff changeset
    16
  val indent: int Config.T
d8da44a8dd25 proper context for various Thy_Output options, via official configuration options in ML and Isar;
wenzelm
parents: 38766
diff changeset
    17
  val source: bool Config.T
d8da44a8dd25 proper context for various Thy_Output options, via official configuration options in ML and Isar;
wenzelm
parents: 38766
diff changeset
    18
  val break: bool Config.T
38766
8891f4520d16 Thy_Output: options based on proper context, although Thy_Output.add_wrapper still allows to maintain old-style wrapper combinators (setmp_CRITICAL etc.);
wenzelm
parents: 37216
diff changeset
    19
  val add_wrapper: ((unit -> string) -> unit -> string) -> Proof.context -> Proof.context
43564
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
    20
  val add_option: binding -> (string -> Proof.context -> Proof.context) -> theory -> theory
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
    21
  val intern_command: theory -> xstring -> string
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
    22
  val defined_command: theory -> string -> bool
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
    23
  val intern_option: theory -> xstring -> string
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
    24
  val defined_option: theory -> string -> bool
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
    25
  val print_antiquotations: Proof.context -> unit
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
    26
  val antiquotation: binding -> 'a context_parser ->
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
    27
    ({source: Args.src, state: Toplevel.state, context: Proof.context} -> 'a -> string) ->
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
    28
      theory -> theory
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
    29
  val boolean: string -> bool
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
    30
  val integer: string -> int
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
    31
  datatype markup = Markup | MarkupEnv | Verbatim
32738
15bb09ca0378 explicit indication of Unsynchronized.ref;
wenzelm
parents: 30683
diff changeset
    32
  val modes: string list Unsynchronized.ref
42508
e21362bf1d93 allow nested @{antiq} (nonterminal) and @@{antiq} terminal;
wenzelm
parents: 42399
diff changeset
    33
  val eval_antiq: Scan.lexicon -> Toplevel.state -> Symbol_Pos.T list * Position.range -> string
30573
49899f26fbd1 de-camelized Symbol_Pos;
wenzelm
parents: 30513
diff changeset
    34
  val eval_antiquote: Scan.lexicon -> Toplevel.state -> Symbol_Pos.text * Position.T -> string
48918
6e5fd4585512 check side-comments of command spans (normally filtered out in Outer_Syntax.toplevel_source);
wenzelm
parents: 47005
diff changeset
    35
  val check_text: Symbol_Pos.text * Position.T -> Toplevel.state -> unit
28427
cc9f7d99fb73 turned process_thy into present_thy, which merely does presentation (wrt. persistent intermediate states);
wenzelm
parents: 28273
diff changeset
    36
  val present_thy: Scan.lexicon -> (string -> string list) -> (markup -> string -> bool) ->
46811
03a2dc9e0624 clarified command span: include trailing whitespace/comments and thus reduce number of ignored spans with associated transactions and states (factor 2);
wenzelm
parents: 46261
diff changeset
    37
    (Toplevel.transition * Toplevel.state) list -> Token.T list -> Buffer.T
38767
d8da44a8dd25 proper context for various Thy_Output options, via official configuration options in ML and Isar;
wenzelm
parents: 38766
diff changeset
    38
  val pretty_text: Proof.context -> string -> Pretty.T
28644
e2ae4a6cf166 ThyOutput: export some auxiliary operations;
wenzelm
parents: 28427
diff changeset
    39
  val pretty_term: Proof.context -> term -> Pretty.T
e2ae4a6cf166 ThyOutput: export some auxiliary operations;
wenzelm
parents: 28427
diff changeset
    40
  val pretty_thm: Proof.context -> thm -> Pretty.T
30390
ad591ee76c78 simplified interface to define document antiquotations, cf. antiquotatation, maybe_pretty_source, output;
wenzelm
parents: 30381
diff changeset
    41
  val str_of_source: Args.src -> string
38767
d8da44a8dd25 proper context for various Thy_Output options, via official configuration options in ML and Isar;
wenzelm
parents: 38766
diff changeset
    42
  val maybe_pretty_source: (Proof.context -> 'a -> Pretty.T) -> Proof.context ->
d8da44a8dd25 proper context for various Thy_Output options, via official configuration options in ML and Isar;
wenzelm
parents: 38766
diff changeset
    43
    Args.src -> 'a list -> Pretty.T list
d8da44a8dd25 proper context for various Thy_Output options, via official configuration options in ML and Isar;
wenzelm
parents: 38766
diff changeset
    44
  val output: Proof.context -> Pretty.T list -> string
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
    45
end;
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
    46
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 37198
diff changeset
    47
structure Thy_Output: THY_OUTPUT =
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
    48
struct
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
    49
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
    50
(** global options **)
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
    51
38767
d8da44a8dd25 proper context for various Thy_Output options, via official configuration options in ML and Isar;
wenzelm
parents: 38766
diff changeset
    52
val display_default = Unsynchronized.ref false;
d8da44a8dd25 proper context for various Thy_Output options, via official configuration options in ML and Isar;
wenzelm
parents: 38766
diff changeset
    53
val quotes_default = Unsynchronized.ref false;
d8da44a8dd25 proper context for various Thy_Output options, via official configuration options in ML and Isar;
wenzelm
parents: 38766
diff changeset
    54
val indent_default = Unsynchronized.ref 0;
d8da44a8dd25 proper context for various Thy_Output options, via official configuration options in ML and Isar;
wenzelm
parents: 38766
diff changeset
    55
val source_default = Unsynchronized.ref false;
d8da44a8dd25 proper context for various Thy_Output options, via official configuration options in ML and Isar;
wenzelm
parents: 38766
diff changeset
    56
val break_default = Unsynchronized.ref false;
d8da44a8dd25 proper context for various Thy_Output options, via official configuration options in ML and Isar;
wenzelm
parents: 38766
diff changeset
    57
42616
92715b528e78 added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents: 42508
diff changeset
    58
val display = Attrib.setup_config_bool (Binding.name "thy_output_display") (fn _ => ! display_default);
92715b528e78 added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents: 42508
diff changeset
    59
val quotes = Attrib.setup_config_bool (Binding.name "thy_output_quotes") (fn _ => ! quotes_default);
92715b528e78 added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents: 42508
diff changeset
    60
val indent = Attrib.setup_config_int (Binding.name "thy_output_indent") (fn _ => ! indent_default);
92715b528e78 added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents: 42508
diff changeset
    61
val source = Attrib.setup_config_bool (Binding.name "thy_output_source") (fn _ => ! source_default);
92715b528e78 added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents: 42508
diff changeset
    62
val break = Attrib.setup_config_bool (Binding.name "thy_output_break") (fn _ => ! break_default);
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
    63
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
    64
38766
8891f4520d16 Thy_Output: options based on proper context, although Thy_Output.add_wrapper still allows to maintain old-style wrapper combinators (setmp_CRITICAL etc.);
wenzelm
parents: 37216
diff changeset
    65
structure Wrappers = Proof_Data
8891f4520d16 Thy_Output: options based on proper context, although Thy_Output.add_wrapper still allows to maintain old-style wrapper combinators (setmp_CRITICAL etc.);
wenzelm
parents: 37216
diff changeset
    66
(
8891f4520d16 Thy_Output: options based on proper context, although Thy_Output.add_wrapper still allows to maintain old-style wrapper combinators (setmp_CRITICAL etc.);
wenzelm
parents: 37216
diff changeset
    67
  type T = ((unit -> string) -> unit -> string) list;
8891f4520d16 Thy_Output: options based on proper context, although Thy_Output.add_wrapper still allows to maintain old-style wrapper combinators (setmp_CRITICAL etc.);
wenzelm
parents: 37216
diff changeset
    68
  fun init _ = [];
8891f4520d16 Thy_Output: options based on proper context, although Thy_Output.add_wrapper still allows to maintain old-style wrapper combinators (setmp_CRITICAL etc.);
wenzelm
parents: 37216
diff changeset
    69
);
8891f4520d16 Thy_Output: options based on proper context, although Thy_Output.add_wrapper still allows to maintain old-style wrapper combinators (setmp_CRITICAL etc.);
wenzelm
parents: 37216
diff changeset
    70
8891f4520d16 Thy_Output: options based on proper context, although Thy_Output.add_wrapper still allows to maintain old-style wrapper combinators (setmp_CRITICAL etc.);
wenzelm
parents: 37216
diff changeset
    71
fun add_wrapper wrapper = Wrappers.map (cons wrapper);
8891f4520d16 Thy_Output: options based on proper context, although Thy_Output.add_wrapper still allows to maintain old-style wrapper combinators (setmp_CRITICAL etc.);
wenzelm
parents: 37216
diff changeset
    72
8891f4520d16 Thy_Output: options based on proper context, although Thy_Output.add_wrapper still allows to maintain old-style wrapper combinators (setmp_CRITICAL etc.);
wenzelm
parents: 37216
diff changeset
    73
val wrap = Wrappers.get #> fold (fn wrapper => fn f => wrapper f);
8891f4520d16 Thy_Output: options based on proper context, although Thy_Output.add_wrapper still allows to maintain old-style wrapper combinators (setmp_CRITICAL etc.);
wenzelm
parents: 37216
diff changeset
    74
8891f4520d16 Thy_Output: options based on proper context, although Thy_Output.add_wrapper still allows to maintain old-style wrapper combinators (setmp_CRITICAL etc.);
wenzelm
parents: 37216
diff changeset
    75
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
    76
30390
ad591ee76c78 simplified interface to define document antiquotations, cf. antiquotatation, maybe_pretty_source, output;
wenzelm
parents: 30381
diff changeset
    77
(** maintain global antiquotations **)
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
    78
43564
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
    79
structure Antiquotations = Theory_Data
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
    80
(
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
    81
  type T =
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
    82
    (Args.src -> Toplevel.state -> Proof.context -> string) Name_Space.table *
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
    83
      (string -> Proof.context -> Proof.context) Name_Space.table;
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
    84
  val empty : T =
45666
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 43947
diff changeset
    85
    (Name_Space.empty_table Isabelle_Markup.doc_antiquotationN,
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 43947
diff changeset
    86
      Name_Space.empty_table Isabelle_Markup.doc_antiquotation_optionN);
43564
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
    87
  val extend = I;
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
    88
  fun merge ((commands1, options1), (commands2, options2)) : T =
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
    89
    (Name_Space.merge_tables (commands1, commands2),
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
    90
      Name_Space.merge_tables (options1, options2));
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
    91
);
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
    92
47005
421760a1efe7 maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents: 46958
diff changeset
    93
fun add_command name cmd thy = thy
421760a1efe7 maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents: 46958
diff changeset
    94
  |> Antiquotations.map (apfst (Name_Space.define (Context.Theory thy) true (name, cmd) #> snd));
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
    95
47005
421760a1efe7 maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents: 46958
diff changeset
    96
fun add_option name opt thy = thy
421760a1efe7 maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents: 46958
diff changeset
    97
  |> Antiquotations.map (apsnd (Name_Space.define (Context.Theory thy) true (name, opt) #> snd));
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
    98
43564
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
    99
val intern_command = Name_Space.intern o #1 o #1 o Antiquotations.get;
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   100
val defined_command = Symtab.defined o #2 o #1 o Antiquotations.get;
26893
44d9960d3587 added defined_command, defined_option;
wenzelm
parents: 26762
diff changeset
   101
43564
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   102
val intern_option = Name_Space.intern o #1 o #2 o Antiquotations.get;
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   103
val defined_option = Symtab.defined o #2 o #2 o Antiquotations.get;
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   104
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   105
fun command src state ctxt =
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   106
  let
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   107
    val thy = Proof_Context.theory_of ctxt;
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   108
    val ((xname, _), pos) = Args.dest_src src;
47005
421760a1efe7 maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents: 46958
diff changeset
   109
    val (name, f) = Name_Space.check (Context.Proof ctxt) (#1 (Antiquotations.get thy)) (xname, pos);
43564
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   110
  in
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   111
    f src state ctxt handle ERROR msg =>
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   112
      cat_error msg ("The error(s) above occurred in document antiquotation: " ^
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   113
        quote name ^ Position.str_of pos)
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   114
  end;
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   115
43564
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   116
fun option ((xname, pos), s) ctxt =
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   117
  let
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   118
    val thy = Proof_Context.theory_of ctxt;
47005
421760a1efe7 maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents: 46958
diff changeset
   119
    val (_, opt) = Name_Space.check (Context.Proof ctxt) (#2 (Antiquotations.get thy)) (xname, pos);
43564
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   120
  in opt s ctxt end;
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   121
43564
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   122
fun print_antiquotations ctxt =
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   123
  let
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   124
    val thy = Proof_Context.theory_of ctxt;
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   125
    val (commands, options) = Antiquotations.get thy;
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   126
    val command_names = map #1 (Name_Space.extern_table ctxt commands);
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   127
    val option_names = map #1 (Name_Space.extern_table ctxt options);
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   128
  in
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   129
    [Pretty.big_list "document antiquotations:" (map Pretty.str command_names),
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   130
      Pretty.big_list "document antiquotation options:" (map Pretty.str option_names)]
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   131
    |> Pretty.chunks |> Pretty.writeln
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   132
  end;
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   133
38766
8891f4520d16 Thy_Output: options based on proper context, although Thy_Output.add_wrapper still allows to maintain old-style wrapper combinators (setmp_CRITICAL etc.);
wenzelm
parents: 37216
diff changeset
   134
fun antiquotation name scan out =
8891f4520d16 Thy_Output: options based on proper context, although Thy_Output.add_wrapper still allows to maintain old-style wrapper combinators (setmp_CRITICAL etc.);
wenzelm
parents: 37216
diff changeset
   135
  add_command name
8891f4520d16 Thy_Output: options based on proper context, although Thy_Output.add_wrapper still allows to maintain old-style wrapper combinators (setmp_CRITICAL etc.);
wenzelm
parents: 37216
diff changeset
   136
    (fn src => fn state => fn ctxt =>
8891f4520d16 Thy_Output: options based on proper context, although Thy_Output.add_wrapper still allows to maintain old-style wrapper combinators (setmp_CRITICAL etc.);
wenzelm
parents: 37216
diff changeset
   137
      let val (x, ctxt') = Args.context_syntax "document antiquotation" scan src ctxt
8891f4520d16 Thy_Output: options based on proper context, although Thy_Output.add_wrapper still allows to maintain old-style wrapper combinators (setmp_CRITICAL etc.);
wenzelm
parents: 37216
diff changeset
   138
      in out {source = src, state = state, context = ctxt'} x end);
30390
ad591ee76c78 simplified interface to define document antiquotations, cf. antiquotatation, maybe_pretty_source, output;
wenzelm
parents: 30381
diff changeset
   139
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   140
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   141
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   142
(** syntax of antiquotations **)
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   143
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   144
(* option values *)
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   145
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   146
fun boolean "" = true
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   147
  | boolean "true" = true
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   148
  | boolean "false" = false
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   149
  | boolean s = error ("Bad boolean value: " ^ quote s);
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   150
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   151
fun integer s =
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   152
  let
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   153
    fun int ss =
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   154
      (case Library.read_int ss of (i, []) => i
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   155
      | _ => error ("Bad integer value: " ^ quote s));
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   156
  in (case Symbol.explode s of "-" :: ss => ~ (int ss) | ss => int ss) end;
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   157
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   158
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   159
(* outer syntax *)
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   160
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   161
local
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   162
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36745
diff changeset
   163
val property =
43564
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   164
  Parse.position Parse.xname -- Scan.optional (Parse.$$$ "=" |-- Parse.!!! Parse.xname) "";
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36745
diff changeset
   165
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36745
diff changeset
   166
val properties =
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36745
diff changeset
   167
  Scan.optional (Parse.$$$ "[" |-- Parse.!!! (Parse.enum "," property --| Parse.$$$ "]")) [];
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   168
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   169
in
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   170
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36745
diff changeset
   171
val antiq =
40800
330eb65c9469 Parse.liberal_name for document antiquotations and attributes;
wenzelm
parents: 39689
diff changeset
   172
  Parse.!!!
330eb65c9469 Parse.liberal_name for document antiquotations and attributes;
wenzelm
parents: 39689
diff changeset
   173
    (Parse.position Parse.liberal_name -- properties -- Args.parse --| Scan.ahead Parse.eof)
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   174
  >> (fn (((x, pos), y), z) => (y, Args.src ((x, z), pos)));
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   175
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   176
end;
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   177
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   178
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   179
(* eval_antiquote *)
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   180
32738
15bb09ca0378 explicit indication of Unsynchronized.ref;
wenzelm
parents: 30683
diff changeset
   181
val modes = Unsynchronized.ref ([]: string list);
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   182
42508
e21362bf1d93 allow nested @{antiq} (nonterminal) and @@{antiq} terminal;
wenzelm
parents: 42399
diff changeset
   183
fun eval_antiq lex state (ss, (pos, _)) =
e21362bf1d93 allow nested @{antiq} (nonterminal) and @@{antiq} terminal;
wenzelm
parents: 42399
diff changeset
   184
  let
e21362bf1d93 allow nested @{antiq} (nonterminal) and @@{antiq} terminal;
wenzelm
parents: 42399
diff changeset
   185
    val (opts, src) = Token.read_antiq lex antiq (ss, pos);
e21362bf1d93 allow nested @{antiq} (nonterminal) and @@{antiq} terminal;
wenzelm
parents: 42399
diff changeset
   186
    fun cmd ctxt = wrap ctxt (fn () => command src state ctxt) ();
e21362bf1d93 allow nested @{antiq} (nonterminal) and @@{antiq} terminal;
wenzelm
parents: 42399
diff changeset
   187
    val preview_ctxt = fold option opts (Toplevel.presentation_context_of state);
e21362bf1d93 allow nested @{antiq} (nonterminal) and @@{antiq} terminal;
wenzelm
parents: 42399
diff changeset
   188
    val print_ctxt = Context_Position.set_visible false preview_ctxt;
e21362bf1d93 allow nested @{antiq} (nonterminal) and @@{antiq} terminal;
wenzelm
parents: 42399
diff changeset
   189
    val _ = cmd preview_ctxt;
e21362bf1d93 allow nested @{antiq} (nonterminal) and @@{antiq} terminal;
wenzelm
parents: 42399
diff changeset
   190
  in Print_Mode.with_modes (! modes @ Latex.modes) (fn () => cmd print_ctxt) () end;
e21362bf1d93 allow nested @{antiq} (nonterminal) and @@{antiq} terminal;
wenzelm
parents: 42399
diff changeset
   191
30367
ee8841b1b981 simplified presentation: pass state directly;
wenzelm
parents: 30317
diff changeset
   192
fun eval_antiquote lex state (txt, pos) =
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   193
  let
30589
cbe27c4ef417 Antiquote.Text: keep full position information;
wenzelm
parents: 30588
diff changeset
   194
    fun expand (Antiquote.Text ss) = Symbol_Pos.content ss
42508
e21362bf1d93 allow nested @{antiq} (nonterminal) and @@{antiq} terminal;
wenzelm
parents: 42399
diff changeset
   195
      | expand (Antiquote.Antiq antiq) = eval_antiq lex state antiq
27344
d44490b06190 Antiquote.Open/Close;
wenzelm
parents: 27258
diff changeset
   196
      | expand (Antiquote.Open _) = ""
d44490b06190 Antiquote.Open/Close;
wenzelm
parents: 27258
diff changeset
   197
      | expand (Antiquote.Close _) = "";
30642
0c9f9c49d5df simplified Antiquote.read (again);
wenzelm
parents: 30635
diff changeset
   198
    val ants = Antiquote.read (Symbol_Pos.explode (txt, pos), pos);
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   199
  in
30635
a7d175c48228 replaced Antiquote.is_antiq by Antiquote.is_text;
wenzelm
parents: 30613
diff changeset
   200
    if Toplevel.is_toplevel state andalso not (forall Antiquote.is_text ants) then
27897
0e7ff439460f report antiquotation names;
wenzelm
parents: 27882
diff changeset
   201
      error ("Unknown context -- cannot expand document antiquotations" ^ Position.str_of pos)
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   202
    else implode (map expand ants)
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   203
  end;
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   204
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   205
48918
6e5fd4585512 check side-comments of command spans (normally filtered out in Outer_Syntax.toplevel_source);
wenzelm
parents: 47005
diff changeset
   206
fun check_text (txt, pos) state =
6e5fd4585512 check side-comments of command spans (normally filtered out in Outer_Syntax.toplevel_source);
wenzelm
parents: 47005
diff changeset
   207
 (Position.report pos Isabelle_Markup.doc_source;
6e5fd4585512 check side-comments of command spans (normally filtered out in Outer_Syntax.toplevel_source);
wenzelm
parents: 47005
diff changeset
   208
  ignore (eval_antiquote (#1 (Keyword.get_lexicons ())) state (txt, pos)));
6e5fd4585512 check side-comments of command spans (normally filtered out in Outer_Syntax.toplevel_source);
wenzelm
parents: 47005
diff changeset
   209
6e5fd4585512 check side-comments of command spans (normally filtered out in Outer_Syntax.toplevel_source);
wenzelm
parents: 47005
diff changeset
   210
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   211
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   212
(** present theory source **)
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   213
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   214
(*NB: arranging white space around command spans is a black art.*)
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   215
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   216
(* presentation tokens *)
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   217
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   218
datatype token =
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   219
    NoToken
36959
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36950
diff changeset
   220
  | BasicToken of Token.T
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   221
  | MarkupToken of string * (string * Position.T)
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   222
  | MarkupEnvToken of string * (string * Position.T)
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   223
  | VerbatimToken of string * Position.T;
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   224
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   225
fun output_token lex state =
30367
ee8841b1b981 simplified presentation: pass state directly;
wenzelm
parents: 30317
diff changeset
   226
  let val eval = eval_antiquote lex state in
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   227
    fn NoToken => ""
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   228
     | BasicToken tok => Latex.output_basic tok
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   229
     | MarkupToken (cmd, txt) => Latex.output_markup cmd (eval txt)
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   230
     | MarkupEnvToken (cmd, txt) => Latex.output_markup_env cmd (eval txt)
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   231
     | VerbatimToken txt => Latex.output_verbatim (eval txt)
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   232
  end;
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   233
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   234
fun basic_token pred (BasicToken tok) = pred tok
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   235
  | basic_token _ _ = false;
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   236
36959
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36950
diff changeset
   237
val improper_token = basic_token (not o Token.is_proper);
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36950
diff changeset
   238
val comment_token = basic_token Token.is_comment;
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36950
diff changeset
   239
val blank_token = basic_token Token.is_blank;
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36950
diff changeset
   240
val newline_token = basic_token Token.is_newline;
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   241
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   242
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   243
(* command spans *)
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   244
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   245
type command = string * Position.T * string list;   (*name, position, tags*)
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   246
type source = (token * (string * int)) list;        (*token, markup flag, meta-comment depth*)
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   247
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   248
datatype span = Span of command * (source * source * source * source) * bool;
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   249
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   250
fun make_span cmd src =
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   251
  let
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   252
    fun take_newline (tok :: toks) =
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   253
          if newline_token (fst tok) then ([tok], toks, true)
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   254
          else ([], tok :: toks, false)
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   255
      | take_newline [] = ([], [], false);
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   256
    val (((src_prefix, src_main), src_suffix1), (src_suffix2, src_appendix, newline)) =
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   257
      src
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   258
      |> take_prefix (improper_token o fst)
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   259
      ||>> take_suffix (improper_token o fst)
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   260
      ||>> take_prefix (comment_token o fst)
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   261
      ||> take_newline;
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   262
  in Span (cmd, (src_prefix, src_main, src_suffix1 @ src_suffix2, src_appendix), newline) end;
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   263
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   264
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   265
(* present spans *)
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   266
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   267
local
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   268
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   269
fun err_bad_nesting pos =
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   270
  error ("Bad nesting of commands in presentation" ^ pos);
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   271
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   272
fun edge which f (x: string option, y) =
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   273
  if x = y then I
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   274
  else (case which (x, y) of NONE => I | SOME txt => Buffer.add (f txt));
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   275
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   276
val begin_tag = edge #2 Latex.begin_tag;
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   277
val end_tag = edge #1 Latex.end_tag;
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   278
fun open_delim delim e = edge #2 Latex.begin_delim e #> delim #> edge #2 Latex.end_delim e;
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   279
fun close_delim delim e = edge #1 Latex.begin_delim e #> delim #> edge #1 Latex.end_delim e;
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   280
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   281
in
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   282
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   283
fun present_span lex default_tags span state state'
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   284
    (tag_stack, active_tag, newline, buffer, present_cont) =
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   285
  let
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   286
    val present = fold (fn (tok, (flag, 0)) =>
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   287
        Buffer.add (output_token lex state' tok)
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   288
        #> Buffer.add flag
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   289
      | _ => I);
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   290
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   291
    val Span ((cmd_name, cmd_pos, cmd_tags), srcs, span_newline) = span;
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   292
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   293
    val (tag, tags) = tag_stack;
46924
wenzelm
parents: 46922
diff changeset
   294
    val tag' = try hd (fold (update (op =)) cmd_tags (the_list tag));
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   295
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   296
    val active_tag' =
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   297
      if is_some tag' then tag'
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   298
      else if cmd_name = "end" andalso not (Toplevel.is_toplevel state') then NONE
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   299
      else try hd (default_tags cmd_name);
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   300
    val edge = (active_tag, active_tag');
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   301
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   302
    val newline' =
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   303
      if is_none active_tag' then span_newline else newline;
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   304
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   305
    val nesting = Toplevel.level state' - Toplevel.level state;
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   306
    val tag_stack' =
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   307
      if nesting = 0 andalso not (Toplevel.is_proof state) then tag_stack
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   308
      else if nesting >= 0 then (tag', replicate nesting tag @ tags)
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   309
      else
33957
e9afca2118d4 normalized uncurry take/drop
haftmann
parents: 33955
diff changeset
   310
        (case drop (~ nesting - 1) tags of
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   311
          tgs :: tgss => (tgs, tgss)
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   312
        | [] => err_bad_nesting (Position.str_of cmd_pos));
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   313
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   314
    val buffer' =
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   315
      buffer
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   316
      |> end_tag edge
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   317
      |> close_delim (fst present_cont) edge
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   318
      |> snd present_cont
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   319
      |> open_delim (present (#1 srcs)) edge
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   320
      |> begin_tag edge
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   321
      |> present (#2 srcs);
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   322
    val present_cont' =
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   323
      if newline then (present (#3 srcs), present (#4 srcs))
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   324
      else (I, present (#3 srcs) #> present (#4 srcs));
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   325
  in (tag_stack', active_tag', newline', buffer', present_cont') end;
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   326
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   327
fun present_trailer ((_, tags), active_tag, _, buffer, present_cont) =
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   328
  if not (null tags) then err_bad_nesting " at end of theory"
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   329
  else
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   330
    buffer
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   331
    |> end_tag (active_tag, NONE)
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   332
    |> close_delim (fst present_cont) (active_tag, NONE)
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   333
    |> snd present_cont;
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   334
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   335
end;
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   336
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   337
28427
cc9f7d99fb73 turned process_thy into present_thy, which merely does presentation (wrt. persistent intermediate states);
wenzelm
parents: 28273
diff changeset
   338
(* present_thy *)
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   339
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   340
datatype markup = Markup | MarkupEnv | Verbatim;
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   341
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   342
local
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   343
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   344
val space_proper =
36959
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36950
diff changeset
   345
  Scan.one Token.is_blank -- Scan.many Token.is_comment -- Scan.one Token.is_proper;
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   346
36959
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36950
diff changeset
   347
val is_improper = not o (Token.is_proper orf Token.is_begin_ignore orf Token.is_end_ignore);
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   348
val improper = Scan.many is_improper;
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   349
val improper_end = Scan.repeat (Scan.unless space_proper (Scan.one is_improper));
36959
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36950
diff changeset
   350
val blank_end = Scan.repeat (Scan.unless space_proper (Scan.one Token.is_blank));
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   351
36959
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36950
diff changeset
   352
val opt_newline = Scan.option (Scan.one Token.is_newline);
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   353
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   354
val ignore =
36959
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36950
diff changeset
   355
  Scan.depend (fn d => opt_newline |-- Scan.one Token.is_begin_ignore
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   356
    >> pair (d + 1)) ||
36959
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36950
diff changeset
   357
  Scan.depend (fn d => Scan.one Token.is_end_ignore --|
43947
9b00f09f7721 defer evaluation of Scan.message, for improved performance in the frequent situation where failure is handled later (e.g. via ||);
wenzelm
parents: 43564
diff changeset
   358
    (if d = 0 then Scan.fail_with (K (fn () => "Bad nesting of meta-comments")) else opt_newline)
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   359
    >> pair (d - 1));
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   360
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36745
diff changeset
   361
val tag = (improper -- Parse.$$$ "%" -- improper) |-- Parse.!!! (Parse.tag_name --| blank_end);
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   362
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   363
val locale =
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36745
diff changeset
   364
  Scan.option ((Parse.$$$ "(" -- improper -- Parse.$$$ "in") |--
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36745
diff changeset
   365
    Parse.!!! (improper |-- Parse.xname --| (improper -- Parse.$$$ ")")));
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   366
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   367
in
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   368
46811
03a2dc9e0624 clarified command span: include trailing whitespace/comments and thus reduce number of ignored spans with associated transactions and states (factor 2);
wenzelm
parents: 46261
diff changeset
   369
fun present_thy lex default_tags is_markup command_results toks =
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   370
  let
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   371
    (* tokens *)
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   372
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   373
    val ignored = Scan.state --| ignore
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   374
      >> (fn d => (NONE, (NoToken, ("", d))));
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   375
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   376
    fun markup mark mk flag = Scan.peek (fn d =>
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36745
diff changeset
   377
      improper |--
46811
03a2dc9e0624 clarified command span: include trailing whitespace/comments and thus reduce number of ignored spans with associated transactions and states (factor 2);
wenzelm
parents: 46261
diff changeset
   378
        Parse.position (Scan.one (Token.is_command andf is_markup mark o Token.content_of)) --
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   379
      Scan.repeat tag --
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36745
diff changeset
   380
      Parse.!!!! ((improper -- locale -- improper) |-- Parse.doc_source --| improper_end)
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   381
      >> (fn (((tok, pos), tags), txt) =>
36959
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36950
diff changeset
   382
        let val name = Token.content_of tok
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   383
        in (SOME (name, pos, tags), (mk (name, txt), (flag, d))) end));
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   384
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   385
    val command = Scan.peek (fn d =>
46811
03a2dc9e0624 clarified command span: include trailing whitespace/comments and thus reduce number of ignored spans with associated transactions and states (factor 2);
wenzelm
parents: 46261
diff changeset
   386
      Parse.position (Scan.one (Token.is_command)) --
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   387
      Scan.repeat tag
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   388
      >> (fn ((tok, pos), tags) =>
36959
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36950
diff changeset
   389
        let val name = Token.content_of tok
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   390
        in (SOME (name, pos, tags), (BasicToken tok, (Latex.markup_false, d))) end));
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   391
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   392
    val cmt = Scan.peek (fn d =>
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36745
diff changeset
   393
      Parse.$$$ "--" |-- Parse.!!!! (improper |-- Parse.doc_source)
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   394
      >> (fn txt => (NONE, (MarkupToken ("cmt", txt), ("", d)))));
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   395
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   396
    val other = Scan.peek (fn d =>
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36745
diff changeset
   397
       Parse.not_eof >> (fn tok => (NONE, (BasicToken tok, ("", d)))));
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   398
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   399
    val token =
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   400
      ignored ||
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   401
      markup Markup MarkupToken Latex.markup_true ||
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   402
      markup MarkupEnv MarkupEnvToken Latex.markup_true ||
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   403
      markup Verbatim (VerbatimToken o #2) "" ||
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   404
      command || cmt || other;
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   405
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   406
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   407
    (* spans *)
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   408
36959
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36950
diff changeset
   409
    val is_eof = fn (_, (BasicToken x, _)) => Token.is_eof x | _ => false;
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36950
diff changeset
   410
    val stopper = Scan.stopper (K (NONE, (BasicToken Token.eof, ("", 0)))) is_eof;
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   411
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   412
    val cmd = Scan.one (is_some o fst);
27732
8dbf5761a24a abstract type Scan.stopper;
wenzelm
parents: 27566
diff changeset
   413
    val non_cmd = Scan.one (is_none o fst andf not o is_eof) >> #2;
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   414
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   415
    val comments = Scan.many (comment_token o fst o snd);
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   416
    val blank = Scan.one (blank_token o fst o snd);
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   417
    val newline = Scan.one (newline_token o fst o snd);
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   418
    val before_cmd =
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   419
      Scan.option (newline -- comments) --
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   420
      Scan.option (newline -- comments) --
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   421
      Scan.option (blank -- comments) -- cmd;
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   422
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   423
    val span =
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   424
      Scan.repeat non_cmd -- cmd --
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   425
        Scan.repeat (Scan.unless before_cmd non_cmd) --
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   426
        Scan.option (newline >> (single o snd))
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   427
      >> (fn (((toks1, (cmd, tok2)), toks3), tok4) =>
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   428
          make_span (the cmd) (toks1 @ (tok2 :: (toks3 @ the_default [] tok4))));
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   429
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   430
    val spans =
46811
03a2dc9e0624 clarified command span: include trailing whitespace/comments and thus reduce number of ignored spans with associated transactions and states (factor 2);
wenzelm
parents: 46261
diff changeset
   431
      Source.of_list (filter_out Token.is_semicolon toks)
36959
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36950
diff changeset
   432
      |> Source.source' 0 Token.stopper (Scan.error (Scan.bulk token)) NONE
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   433
      |> Source.source stopper (Scan.error (Scan.bulk span)) NONE
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   434
      |> Source.exhaust;
28427
cc9f7d99fb73 turned process_thy into present_thy, which merely does presentation (wrt. persistent intermediate states);
wenzelm
parents: 28273
diff changeset
   435
cc9f7d99fb73 turned process_thy into present_thy, which merely does presentation (wrt. persistent intermediate states);
wenzelm
parents: 28273
diff changeset
   436
cc9f7d99fb73 turned process_thy into present_thy, which merely does presentation (wrt. persistent intermediate states);
wenzelm
parents: 28273
diff changeset
   437
    (* present commands *)
cc9f7d99fb73 turned process_thy into present_thy, which merely does presentation (wrt. persistent intermediate states);
wenzelm
parents: 28273
diff changeset
   438
cc9f7d99fb73 turned process_thy into present_thy, which merely does presentation (wrt. persistent intermediate states);
wenzelm
parents: 28273
diff changeset
   439
    fun present_command tr span st st' =
cc9f7d99fb73 turned process_thy into present_thy, which merely does presentation (wrt. persistent intermediate states);
wenzelm
parents: 28273
diff changeset
   440
      Toplevel.setmp_thread_position tr (present_span lex default_tags span st st');
cc9f7d99fb73 turned process_thy into present_thy, which merely does presentation (wrt. persistent intermediate states);
wenzelm
parents: 28273
diff changeset
   441
cc9f7d99fb73 turned process_thy into present_thy, which merely does presentation (wrt. persistent intermediate states);
wenzelm
parents: 28273
diff changeset
   442
    fun present _ [] = I
cc9f7d99fb73 turned process_thy into present_thy, which merely does presentation (wrt. persistent intermediate states);
wenzelm
parents: 28273
diff changeset
   443
      | present st (((tr, st'), span) :: rest) = present_command tr span st st' #> present st' rest;
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   444
  in
28427
cc9f7d99fb73 turned process_thy into present_thy, which merely does presentation (wrt. persistent intermediate states);
wenzelm
parents: 28273
diff changeset
   445
    if length command_results = length spans then
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   446
      ((NONE, []), NONE, true, Buffer.empty, (I, I))
28427
cc9f7d99fb73 turned process_thy into present_thy, which merely does presentation (wrt. persistent intermediate states);
wenzelm
parents: 28273
diff changeset
   447
      |> present Toplevel.toplevel (command_results ~~ spans)
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   448
      |> present_trailer
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   449
    else error "Messed-up outer syntax for presentation"
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   450
  end;
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   451
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   452
end;
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   453
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   454
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   455
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   456
(** setup default output **)
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   457
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   458
(* options *)
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   459
43564
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   460
val _ =
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   461
  Context.>> (Context.map_theory
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   462
   (add_option (Binding.name "show_types") (Config.put show_types o boolean) #>
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   463
    add_option (Binding.name "show_sorts") (Config.put show_sorts o boolean) #>
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   464
    add_option (Binding.name "show_structs") (Config.put show_structs o boolean) #>
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   465
    add_option (Binding.name "show_question_marks") (Config.put show_question_marks o boolean) #>
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   466
    add_option (Binding.name "show_abbrevs") (Config.put show_abbrevs o boolean) #>
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   467
    add_option (Binding.name "names_long") (Config.put Name_Space.names_long o boolean) #>
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   468
    add_option (Binding.name "names_short") (Config.put Name_Space.names_short o boolean) #>
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   469
    add_option (Binding.name "names_unique") (Config.put Name_Space.names_unique o boolean) #>
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   470
    add_option (Binding.name "eta_contract") (Config.put Syntax_Trans.eta_contract o boolean) #>
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   471
    add_option (Binding.name "display") (Config.put display o boolean) #>
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   472
    add_option (Binding.name "break") (Config.put break o boolean) #>
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   473
    add_option (Binding.name "quotes") (Config.put quotes o boolean) #>
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   474
    add_option (Binding.name "mode") (add_wrapper o Print_Mode.with_modes o single) #>
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   475
    add_option (Binding.name "margin") (add_wrapper o setmp_CRITICAL Pretty.margin_default o integer) #>
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   476
    add_option (Binding.name "indent") (Config.put indent o integer) #>
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   477
    add_option (Binding.name "source") (Config.put source o boolean) #>
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   478
    add_option (Binding.name "goals_limit") (Config.put Goal_Display.goals_limit o integer)));
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   479
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   480
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   481
(* basic pretty printing *)
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   482
38767
d8da44a8dd25 proper context for various Thy_Output options, via official configuration options in ML and Isar;
wenzelm
parents: 38766
diff changeset
   483
fun tweak_line ctxt s =
d8da44a8dd25 proper context for various Thy_Output options, via official configuration options in ML and Isar;
wenzelm
parents: 38766
diff changeset
   484
  if Config.get ctxt display then s else Symbol.strip_blanks s;
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   485
38767
d8da44a8dd25 proper context for various Thy_Output options, via official configuration options in ML and Isar;
wenzelm
parents: 38766
diff changeset
   486
fun pretty_text ctxt =
46195
wenzelm
parents: 45666
diff changeset
   487
  Pretty.chunks o map Pretty.str o map (tweak_line ctxt) o split_lines;
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   488
26710
f79aa228c582 pretty_term: no revert_skolems here, but auto_fixes (token translations will do the rest);
wenzelm
parents: 26455
diff changeset
   489
fun pretty_term ctxt t = Syntax.pretty_term (Variable.auto_fixes t ctxt) t;
24920
2a45e400fdad generic Syntax.pretty/string_of operations;
wenzelm
parents: 24680
diff changeset
   490
32898
e871d897969c term styles also cover antiquotations term_type and typeof
haftmann
parents: 32890
diff changeset
   491
fun pretty_thm ctxt = pretty_term ctxt o Thm.full_prop_of;
e871d897969c term styles also cover antiquotations term_type and typeof
haftmann
parents: 32890
diff changeset
   492
e871d897969c term styles also cover antiquotations term_type and typeof
haftmann
parents: 32890
diff changeset
   493
fun pretty_term_style ctxt (style, t) =
e871d897969c term styles also cover antiquotations term_type and typeof
haftmann
parents: 32890
diff changeset
   494
  pretty_term ctxt (style t);
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   495
32898
e871d897969c term styles also cover antiquotations term_type and typeof
haftmann
parents: 32890
diff changeset
   496
fun pretty_thm_style ctxt (style, th) =
e871d897969c term styles also cover antiquotations term_type and typeof
haftmann
parents: 32890
diff changeset
   497
  pretty_term ctxt (style (Thm.full_prop_of th));
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   498
32898
e871d897969c term styles also cover antiquotations term_type and typeof
haftmann
parents: 32890
diff changeset
   499
fun pretty_term_typ ctxt (style, t) =
e871d897969c term styles also cover antiquotations term_type and typeof
haftmann
parents: 32890
diff changeset
   500
  let val t' = style t
39288
f1ae2493d93f eliminated aliases of Type.constraint;
wenzelm
parents: 39134
diff changeset
   501
  in pretty_term ctxt (Type.constraint (Term.fastype_of t') t') end;
32898
e871d897969c term styles also cover antiquotations term_type and typeof
haftmann
parents: 32890
diff changeset
   502
e871d897969c term styles also cover antiquotations term_type and typeof
haftmann
parents: 32890
diff changeset
   503
fun pretty_term_typeof ctxt (style, t) =
e871d897969c term styles also cover antiquotations term_type and typeof
haftmann
parents: 32890
diff changeset
   504
  Syntax.pretty_typ ctxt (Term.fastype_of (style t));
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   505
25373
ccbf65080fdf @{const}: improved ProofContext.read_const does the job;
wenzelm
parents: 25241
diff changeset
   506
fun pretty_const ctxt c =
ccbf65080fdf @{const}: improved ProofContext.read_const does the job;
wenzelm
parents: 25241
diff changeset
   507
  let
42360
da8817d01e7c modernized structure Proof_Context;
wenzelm
parents: 42359
diff changeset
   508
    val t = Const (c, Consts.type_scheme (Proof_Context.consts_of ctxt) c)
25373
ccbf65080fdf @{const}: improved ProofContext.read_const does the job;
wenzelm
parents: 25241
diff changeset
   509
      handle TYPE (msg, _, _) => error msg;
ccbf65080fdf @{const}: improved ProofContext.read_const does the job;
wenzelm
parents: 25241
diff changeset
   510
    val ([t'], _) = Variable.import_terms true [t] ctxt;
ccbf65080fdf @{const}: improved ProofContext.read_const does the job;
wenzelm
parents: 25241
diff changeset
   511
  in pretty_term ctxt t' end;
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   512
25407
2859cf34aaf0 abbrev: bypass full term check via ProofContext.standard_infer_types (prevents forced expansion);
wenzelm
parents: 25373
diff changeset
   513
fun pretty_abbrev ctxt s =
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   514
  let
42399
95b17b4901b5 pretty_abbrev: read abbreviation more directly;
wenzelm
parents: 42360
diff changeset
   515
    val t = Syntax.read_term (Proof_Context.set_mode Proof_Context.mode_abbrev ctxt) s;
24920
2a45e400fdad generic Syntax.pretty/string_of operations;
wenzelm
parents: 24680
diff changeset
   516
    fun err () = error ("Abbreviated constant expected: " ^ Syntax.string_of_term ctxt t);
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   517
    val (head, args) = Term.strip_comb t;
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   518
    val (c, T) = Term.dest_Const head handle TERM _ => err ();
42360
da8817d01e7c modernized structure Proof_Context;
wenzelm
parents: 42359
diff changeset
   519
    val (U, u) = Consts.the_abbreviation (Proof_Context.consts_of ctxt) c
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   520
      handle TYPE _ => err ();
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   521
    val t' = Term.betapplys (Envir.expand_atom T (U, u), args);
32898
e871d897969c term styles also cover antiquotations term_type and typeof
haftmann
parents: 32890
diff changeset
   522
    val eq = Logic.mk_equals (t, t');
e871d897969c term styles also cover antiquotations term_type and typeof
haftmann
parents: 32890
diff changeset
   523
    val ctxt' = Variable.auto_fixes eq ctxt;
42360
da8817d01e7c modernized structure Proof_Context;
wenzelm
parents: 42359
diff changeset
   524
  in Proof_Context.pretty_term_abbrev ctxt' eq end;
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   525
39305
d4fa19eb0822 'class' and 'type' are now antiquoations by default
haftmann
parents: 39134
diff changeset
   526
fun pretty_class ctxt =
42360
da8817d01e7c modernized structure Proof_Context;
wenzelm
parents: 42359
diff changeset
   527
  Pretty.str o Proof_Context.extern_class ctxt o Proof_Context.read_class ctxt;
39305
d4fa19eb0822 'class' and 'type' are now antiquoations by default
haftmann
parents: 39134
diff changeset
   528
39309
74469faa27ca type antiquotation: allow arbitrary type abbreviations, but fail with user-space exception on bad input
haftmann
parents: 39308
diff changeset
   529
fun pretty_type ctxt s =
42360
da8817d01e7c modernized structure Proof_Context;
wenzelm
parents: 42359
diff changeset
   530
  let val Type (name, _) = Proof_Context.read_type_name_proper ctxt false s
da8817d01e7c modernized structure Proof_Context;
wenzelm
parents: 42359
diff changeset
   531
  in Pretty.str (Proof_Context.extern_type ctxt name) end;
39305
d4fa19eb0822 'class' and 'type' are now antiquoations by default
haftmann
parents: 39134
diff changeset
   532
33388
d64545e6cba5 modernized structure Proof_Syntax;
wenzelm
parents: 33095
diff changeset
   533
fun pretty_prf full ctxt = Proof_Syntax.pretty_proof_of ctxt full;
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   534
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   535
fun pretty_theory ctxt name =
42360
da8817d01e7c modernized structure Proof_Context;
wenzelm
parents: 42359
diff changeset
   536
  (Theory.requires (Proof_Context.theory_of ctxt) name "presentation"; Pretty.str name);
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   537
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   538
30390
ad591ee76c78 simplified interface to define document antiquotations, cf. antiquotatation, maybe_pretty_source, output;
wenzelm
parents: 30381
diff changeset
   539
(* default output *)
ad591ee76c78 simplified interface to define document antiquotations, cf. antiquotatation, maybe_pretty_source, output;
wenzelm
parents: 30381
diff changeset
   540
36959
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36950
diff changeset
   541
val str_of_source = space_implode " " o map Token.unparse o #2 o #1 o Args.dest_src;
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   542
38767
d8da44a8dd25 proper context for various Thy_Output options, via official configuration options in ML and Isar;
wenzelm
parents: 38766
diff changeset
   543
fun maybe_pretty_source pretty ctxt src xs =
d8da44a8dd25 proper context for various Thy_Output options, via official configuration options in ML and Isar;
wenzelm
parents: 38766
diff changeset
   544
  map (pretty ctxt) xs  (*always pretty in order to exhibit errors!*)
d8da44a8dd25 proper context for various Thy_Output options, via official configuration options in ML and Isar;
wenzelm
parents: 38766
diff changeset
   545
  |> (if Config.get ctxt source then K [pretty_text ctxt (str_of_source src)] else I);
30390
ad591ee76c78 simplified interface to define document antiquotations, cf. antiquotatation, maybe_pretty_source, output;
wenzelm
parents: 30381
diff changeset
   546
38767
d8da44a8dd25 proper context for various Thy_Output options, via official configuration options in ML and Isar;
wenzelm
parents: 38766
diff changeset
   547
fun output ctxt prts =
30390
ad591ee76c78 simplified interface to define document antiquotations, cf. antiquotatation, maybe_pretty_source, output;
wenzelm
parents: 30381
diff changeset
   548
  prts
38767
d8da44a8dd25 proper context for various Thy_Output options, via official configuration options in ML and Isar;
wenzelm
parents: 38766
diff changeset
   549
  |> (if Config.get ctxt quotes then map Pretty.quote else I)
d8da44a8dd25 proper context for various Thy_Output options, via official configuration options in ML and Isar;
wenzelm
parents: 38766
diff changeset
   550
  |> (if Config.get ctxt display then
d8da44a8dd25 proper context for various Thy_Output options, via official configuration options in ML and Isar;
wenzelm
parents: 38766
diff changeset
   551
    map (Output.output o Pretty.string_of o Pretty.indent (Config.get ctxt indent))
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   552
    #> space_implode "\\isasep\\isanewline%\n"
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   553
    #> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   554
  else
38767
d8da44a8dd25 proper context for various Thy_Output options, via official configuration options in ML and Isar;
wenzelm
parents: 38766
diff changeset
   555
    map (Output.output o (if Config.get ctxt break then Pretty.string_of else Pretty.str_of))
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   556
    #> space_implode "\\isasep\\isanewline%\n"
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   557
    #> enclose "\\isa{" "}");
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   558
30390
ad591ee76c78 simplified interface to define document antiquotations, cf. antiquotatation, maybe_pretty_source, output;
wenzelm
parents: 30381
diff changeset
   559
ad591ee76c78 simplified interface to define document antiquotations, cf. antiquotatation, maybe_pretty_source, output;
wenzelm
parents: 30381
diff changeset
   560
ad591ee76c78 simplified interface to define document antiquotations, cf. antiquotatation, maybe_pretty_source, output;
wenzelm
parents: 30381
diff changeset
   561
(** concrete antiquotations **)
ad591ee76c78 simplified interface to define document antiquotations, cf. antiquotatation, maybe_pretty_source, output;
wenzelm
parents: 30381
diff changeset
   562
ad591ee76c78 simplified interface to define document antiquotations, cf. antiquotatation, maybe_pretty_source, output;
wenzelm
parents: 30381
diff changeset
   563
(* basic entities *)
ad591ee76c78 simplified interface to define document antiquotations, cf. antiquotatation, maybe_pretty_source, output;
wenzelm
parents: 30381
diff changeset
   564
ad591ee76c78 simplified interface to define document antiquotations, cf. antiquotatation, maybe_pretty_source, output;
wenzelm
parents: 30381
diff changeset
   565
local
ad591ee76c78 simplified interface to define document antiquotations, cf. antiquotatation, maybe_pretty_source, output;
wenzelm
parents: 30381
diff changeset
   566
ad591ee76c78 simplified interface to define document antiquotations, cf. antiquotatation, maybe_pretty_source, output;
wenzelm
parents: 30381
diff changeset
   567
fun basic_entities name scan pretty = antiquotation name scan
38767
d8da44a8dd25 proper context for various Thy_Output options, via official configuration options in ML and Isar;
wenzelm
parents: 38766
diff changeset
   568
  (fn {source, context, ...} => output context o maybe_pretty_source pretty context source);
30390
ad591ee76c78 simplified interface to define document antiquotations, cf. antiquotatation, maybe_pretty_source, output;
wenzelm
parents: 30381
diff changeset
   569
32890
77df12652210 generalized term styles: transformations may depend on arguments; modernized term_style module; antiquotations thm, prop and term accepting term styles
haftmann
parents: 32738
diff changeset
   570
fun basic_entities_style name scan pretty = antiquotation name scan
77df12652210 generalized term styles: transformations may depend on arguments; modernized term_style module; antiquotations thm, prop and term accepting term styles
haftmann
parents: 32738
diff changeset
   571
  (fn {source, context, ...} => fn (style, xs) =>
38767
d8da44a8dd25 proper context for various Thy_Output options, via official configuration options in ML and Isar;
wenzelm
parents: 38766
diff changeset
   572
    output context
d8da44a8dd25 proper context for various Thy_Output options, via official configuration options in ML and Isar;
wenzelm
parents: 38766
diff changeset
   573
      (maybe_pretty_source (fn ctxt => fn x => pretty ctxt (style, x)) context source xs));
32890
77df12652210 generalized term styles: transformations may depend on arguments; modernized term_style module; antiquotations thm, prop and term accepting term styles
haftmann
parents: 32738
diff changeset
   574
30390
ad591ee76c78 simplified interface to define document antiquotations, cf. antiquotatation, maybe_pretty_source, output;
wenzelm
parents: 30381
diff changeset
   575
fun basic_entity name scan = basic_entities name (scan >> single);
ad591ee76c78 simplified interface to define document antiquotations, cf. antiquotatation, maybe_pretty_source, output;
wenzelm
parents: 30381
diff changeset
   576
ad591ee76c78 simplified interface to define document antiquotations, cf. antiquotatation, maybe_pretty_source, output;
wenzelm
parents: 30381
diff changeset
   577
in
ad591ee76c78 simplified interface to define document antiquotations, cf. antiquotatation, maybe_pretty_source, output;
wenzelm
parents: 30381
diff changeset
   578
43564
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   579
val _ =
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   580
  Context.>> (Context.map_theory
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   581
   (basic_entities_style (Binding.name "thm") (Term_Style.parse -- Attrib.thms) pretty_thm_style #>
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   582
    basic_entity (Binding.name "prop") (Term_Style.parse -- Args.prop) pretty_term_style #>
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   583
    basic_entity (Binding.name "term") (Term_Style.parse -- Args.term) pretty_term_style #>
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   584
    basic_entity (Binding.name "term_type") (Term_Style.parse -- Args.term) pretty_term_typ #>
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   585
    basic_entity (Binding.name "typeof") (Term_Style.parse -- Args.term) pretty_term_typeof #>
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   586
    basic_entity (Binding.name "const") (Args.const_proper false) pretty_const #>
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   587
    basic_entity (Binding.name "abbrev") (Scan.lift Args.name_source) pretty_abbrev #>
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   588
    basic_entity (Binding.name "typ") Args.typ_abbrev Syntax.pretty_typ #>
46922
3717f3878714 source positions for locale and class expressions;
wenzelm
parents: 46811
diff changeset
   589
    basic_entity (Binding.name "class") (Scan.lift Args.name_source) pretty_class #>
43564
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   590
    basic_entity (Binding.name "type") (Scan.lift Args.name) pretty_type #>
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   591
    basic_entity (Binding.name "text") (Scan.lift Args.name) pretty_text #>
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   592
    basic_entities (Binding.name "prf") Attrib.thms (pretty_prf false) #>
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   593
    basic_entities (Binding.name "full_prf") Attrib.thms (pretty_prf true) #>
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   594
    basic_entity (Binding.name "theory") (Scan.lift Args.name) pretty_theory #>
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   595
    basic_entities_style (Binding.name "thm_style")
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   596
      (Term_Style.parse_bare -- Attrib.thms) pretty_thm_style #>
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   597
    basic_entity (Binding.name "term_style")
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   598
      (Term_Style.parse_bare -- Args.term) pretty_term_style));
32898
e871d897969c term styles also cover antiquotations term_type and typeof
haftmann
parents: 32890
diff changeset
   599
30390
ad591ee76c78 simplified interface to define document antiquotations, cf. antiquotatation, maybe_pretty_source, output;
wenzelm
parents: 30381
diff changeset
   600
end;
ad591ee76c78 simplified interface to define document antiquotations, cf. antiquotatation, maybe_pretty_source, output;
wenzelm
parents: 30381
diff changeset
   601
ad591ee76c78 simplified interface to define document antiquotations, cf. antiquotatation, maybe_pretty_source, output;
wenzelm
parents: 30381
diff changeset
   602
ad591ee76c78 simplified interface to define document antiquotations, cf. antiquotatation, maybe_pretty_source, output;
wenzelm
parents: 30381
diff changeset
   603
(* goal state *)
ad591ee76c78 simplified interface to define document antiquotations, cf. antiquotatation, maybe_pretty_source, output;
wenzelm
parents: 30381
diff changeset
   604
ad591ee76c78 simplified interface to define document antiquotations, cf. antiquotatation, maybe_pretty_source, output;
wenzelm
parents: 30381
diff changeset
   605
local
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   606
30367
ee8841b1b981 simplified presentation: pass state directly;
wenzelm
parents: 30317
diff changeset
   607
fun proof_state state =
ee8841b1b981 simplified presentation: pass state directly;
wenzelm
parents: 30317
diff changeset
   608
  (case try Toplevel.proof_of state of
ee8841b1b981 simplified presentation: pass state directly;
wenzelm
parents: 30317
diff changeset
   609
    SOME prf => prf
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   610
  | _ => error "No proof state");
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   611
30390
ad591ee76c78 simplified interface to define document antiquotations, cf. antiquotatation, maybe_pretty_source, output;
wenzelm
parents: 30381
diff changeset
   612
fun goal_state name main_goal = antiquotation name (Scan.succeed ())
39125
f45d332a90e3 pretty_goals: turned some global references and function arguments into configuration options (goals_limit = 10, goals_total = true, show_main_goal = false) depending on the context;
wenzelm
parents: 38980
diff changeset
   613
  (fn {state, context = ctxt, ...} => fn () => output ctxt
39129
976af4e27cde recovered options for goal antiquotations from f45d332a90e3: actually pass context to Proof.pretty_goals (see also 45facd8f358e);
wenzelm
parents: 39128
diff changeset
   614
    [Pretty.chunks
976af4e27cde recovered options for goal antiquotations from f45d332a90e3: actually pass context to Proof.pretty_goals (see also 45facd8f358e);
wenzelm
parents: 39128
diff changeset
   615
      (Proof.pretty_goals main_goal (Proof.map_context (K ctxt) (proof_state state)))]);
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   616
30390
ad591ee76c78 simplified interface to define document antiquotations, cf. antiquotatation, maybe_pretty_source, output;
wenzelm
parents: 30381
diff changeset
   617
in
ad591ee76c78 simplified interface to define document antiquotations, cf. antiquotatation, maybe_pretty_source, output;
wenzelm
parents: 30381
diff changeset
   618
43564
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   619
val _ =
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   620
  Context.>> (Context.map_theory
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   621
   (goal_state (Binding.name "goals") true #>
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   622
    goal_state (Binding.name "subgoals") false));
30390
ad591ee76c78 simplified interface to define document antiquotations, cf. antiquotatation, maybe_pretty_source, output;
wenzelm
parents: 30381
diff changeset
   623
ad591ee76c78 simplified interface to define document antiquotations, cf. antiquotatation, maybe_pretty_source, output;
wenzelm
parents: 30381
diff changeset
   624
end;
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   625
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   626
30390
ad591ee76c78 simplified interface to define document antiquotations, cf. antiquotatation, maybe_pretty_source, output;
wenzelm
parents: 30381
diff changeset
   627
(* embedded lemma *)
27522
b819d3b263a0 @{lemma}: allow terminal method;
wenzelm
parents: 27381
diff changeset
   628
46958
0ec8f04e753a define keywords early when processing the theory header, before running the body commands;
wenzelm
parents: 46957
diff changeset
   629
val _ = Keyword.define ("by", NONE);  (*overlap with command category*)
46950
d0181abdbdac declare command keywords via theory header, including strict checking outside Pure;
wenzelm
parents: 46947
diff changeset
   630
43564
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   631
val _ =
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   632
  Context.>> (Context.map_theory
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   633
   (antiquotation (Binding.name "lemma")
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   634
    (Args.prop -- Scan.lift (Args.$$$ "by" |-- Method.parse -- Scan.option Method.parse))
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   635
    (fn {source, context, ...} => fn (prop, methods) =>
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   636
      let
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   637
        val prop_src =
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   638
          (case Args.dest_src source of ((a, arg :: _), pos) => Args.src ((a, [arg]), pos));
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   639
        (* FIXME check proof!? *)
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   640
        val _ = context
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   641
          |> Proof.theorem NONE (K I) [[(prop, [])]]
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   642
          |> Proof.global_terminal_proof methods;
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   643
      in output context (maybe_pretty_source pretty_term context prop_src [prop]) end)));
30390
ad591ee76c78 simplified interface to define document antiquotations, cf. antiquotatation, maybe_pretty_source, output;
wenzelm
parents: 30381
diff changeset
   644
ad591ee76c78 simplified interface to define document antiquotations, cf. antiquotatation, maybe_pretty_source, output;
wenzelm
parents: 30381
diff changeset
   645
ad591ee76c78 simplified interface to define document antiquotations, cf. antiquotatation, maybe_pretty_source, output;
wenzelm
parents: 30381
diff changeset
   646
(* ML text *)
ad591ee76c78 simplified interface to define document antiquotations, cf. antiquotatation, maybe_pretty_source, output;
wenzelm
parents: 30381
diff changeset
   647
40801
6cfacec435e6 added document antiquotation @{file};
wenzelm
parents: 40800
diff changeset
   648
val verb_text =
6cfacec435e6 added document antiquotation @{file};
wenzelm
parents: 40800
diff changeset
   649
  split_lines
6cfacec435e6 added document antiquotation @{file};
wenzelm
parents: 40800
diff changeset
   650
  #> map (space_implode "\\verb,|," o map (enclose "\\verb|" "|") o space_explode "|")
6cfacec435e6 added document antiquotation @{file};
wenzelm
parents: 40800
diff changeset
   651
  #> space_implode "\\isasep\\isanewline%\n";
6cfacec435e6 added document antiquotation @{file};
wenzelm
parents: 40800
diff changeset
   652
30390
ad591ee76c78 simplified interface to define document antiquotations, cf. antiquotatation, maybe_pretty_source, output;
wenzelm
parents: 30381
diff changeset
   653
local
ad591ee76c78 simplified interface to define document antiquotations, cf. antiquotatation, maybe_pretty_source, output;
wenzelm
parents: 30381
diff changeset
   654
ad591ee76c78 simplified interface to define document antiquotations, cf. antiquotatation, maybe_pretty_source, output;
wenzelm
parents: 30381
diff changeset
   655
fun ml_text name ml = antiquotation name (Scan.lift Args.name_source_position)
ad591ee76c78 simplified interface to define document antiquotations, cf. antiquotatation, maybe_pretty_source, output;
wenzelm
parents: 30381
diff changeset
   656
  (fn {context, ...} => fn (txt, pos) =>
37198
3af985b10550 replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information;
wenzelm
parents: 37146
diff changeset
   657
   (ML_Context.eval_in (SOME context) false pos (ml pos txt);
30573
49899f26fbd1 de-camelized Symbol_Pos;
wenzelm
parents: 30513
diff changeset
   658
    Symbol_Pos.content (Symbol_Pos.explode (txt, pos))
38767
d8da44a8dd25 proper context for various Thy_Output options, via official configuration options in ML and Isar;
wenzelm
parents: 38766
diff changeset
   659
    |> (if Config.get context quotes then quote else I)
d8da44a8dd25 proper context for various Thy_Output options, via official configuration options in ML and Isar;
wenzelm
parents: 38766
diff changeset
   660
    |> (if Config.get context display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
40801
6cfacec435e6 added document antiquotation @{file};
wenzelm
parents: 40800
diff changeset
   661
        else verb_text)));
30390
ad591ee76c78 simplified interface to define document antiquotations, cf. antiquotatation, maybe_pretty_source, output;
wenzelm
parents: 30381
diff changeset
   662
37198
3af985b10550 replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information;
wenzelm
parents: 37146
diff changeset
   663
fun ml_enclose bg en pos txt =
3af985b10550 replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information;
wenzelm
parents: 37146
diff changeset
   664
  ML_Lex.read Position.none bg @ ML_Lex.read pos txt @ ML_Lex.read Position.none en;
3af985b10550 replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information;
wenzelm
parents: 37146
diff changeset
   665
30390
ad591ee76c78 simplified interface to define document antiquotations, cf. antiquotatation, maybe_pretty_source, output;
wenzelm
parents: 30381
diff changeset
   666
in
ad591ee76c78 simplified interface to define document antiquotations, cf. antiquotatation, maybe_pretty_source, output;
wenzelm
parents: 30381
diff changeset
   667
43564
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   668
val _ =
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   669
  Context.>> (Context.map_theory
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   670
   (ml_text (Binding.name "ML") (ml_enclose "fn _ => (" ");") #>
46261
b03897da3c90 document antiquotations for ML infix operators;
wenzelm
parents: 46195
diff changeset
   671
    ml_text (Binding.name "ML_op") (ml_enclose "fn _ => (op " ");") #>
43564
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   672
    ml_text (Binding.name "ML_type") (ml_enclose "val _ = NONE : (" ") option;") #>
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   673
    ml_text (Binding.name "ML_struct")
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   674
      (ml_enclose "functor XXX() = struct structure XX = " " end;") #>
37198
3af985b10550 replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information;
wenzelm
parents: 37146
diff changeset
   675
43564
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   676
    ml_text (Binding.name "ML_functor")   (* FIXME formal treatment of functor name (!?) *)
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   677
      (fn pos => fn txt =>
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   678
        ML_Lex.read Position.none ("ML_Env.check_functor " ^
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   679
          ML_Syntax.print_string (Symbol_Pos.content (Symbol_Pos.explode (txt, pos))))) #>
37198
3af985b10550 replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information;
wenzelm
parents: 37146
diff changeset
   680
43564
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   681
    ml_text (Binding.name "ML_text") (K (K []))));
22124
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   682
27b674312b2f renamed Isar/isar_output.ML to Thy/thy_output.ML;
wenzelm
parents:
diff changeset
   683
end;
30390
ad591ee76c78 simplified interface to define document antiquotations, cf. antiquotatation, maybe_pretty_source, output;
wenzelm
parents: 30381
diff changeset
   684
40801
6cfacec435e6 added document antiquotation @{file};
wenzelm
parents: 40800
diff changeset
   685
6cfacec435e6 added document antiquotation @{file};
wenzelm
parents: 40800
diff changeset
   686
(* files *)
6cfacec435e6 added document antiquotation @{file};
wenzelm
parents: 40800
diff changeset
   687
43564
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   688
val _ =
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   689
  Context.>> (Context.map_theory
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   690
   (antiquotation (Binding.name "file") (Scan.lift Args.name)
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   691
    (fn _ => fn path =>
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   692
      if File.exists (Path.explode path) then verb_text path
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 42669
diff changeset
   693
      else error ("Bad file: " ^ quote path))));
40801
6cfacec435e6 added document antiquotation @{file};
wenzelm
parents: 40800
diff changeset
   694
30390
ad591ee76c78 simplified interface to define document antiquotations, cf. antiquotatation, maybe_pretty_source, output;
wenzelm
parents: 30381
diff changeset
   695
end;