src/Pure/Isar/isar_output.ML
author wenzelm
Mon, 04 Sep 2000 18:38:53 +0200
changeset 9828 1d8bc4f1833e
parent 9750 270cd9831e7b
child 9863 67cdb658e422
permissions -rw-r--r--
display: avoid empty lines;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
9140
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/Isar/isar_output.ML
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
     3
    Author:     Markus Wenzel, TU Muenchen
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
     5
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
     6
Isar theory output.
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
     7
*)
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
     8
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
     9
signature ISAR_OUTPUT =
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    10
sig
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    11
  val add_commands: (string * (Args.src -> Proof.context -> string)) list -> unit
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    12
  val add_options: (string * (string -> (unit -> string) -> unit -> string)) list -> unit
9220
d0506ced27c8 added options "eta_contract", "long_names";
wenzelm
parents: 9213
diff changeset
    13
  val print_antiquotations: unit -> unit
9140
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    14
  val boolean: string -> bool
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    15
  val integer: string -> int
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    16
  val args: (Proof.context * Args.T list -> 'a * (Proof.context * Args.T list)) ->
9750
270cd9831e7b added "source" option;
wenzelm
parents: 9732
diff changeset
    17
    (Args.src -> Proof.context -> 'a -> string) -> Args.src -> Proof.context -> string
9140
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    18
  datatype markup = Markup | MarkupEnv | Verbatim
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    19
  val interest_level: int ref
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    20
  val parse_thy: (markup -> OuterLex.token list -> OuterLex.token * OuterLex.token list) ->
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    21
    Scan.lexicon -> Toplevel.transition list -> (OuterLex.token, 'a) Source.source ->
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    22
      (Toplevel.transition * (Toplevel.state -> Buffer.T -> Buffer.T)) list * Buffer.T
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    23
  val display: bool ref
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    24
  val quotes: bool ref
9732
c32c7ef228c6 added "name" antiq and "indent" option;
wenzelm
parents: 9504
diff changeset
    25
  val indent: int ref
9750
270cd9831e7b added "source" option;
wenzelm
parents: 9732
diff changeset
    26
  val source: bool ref
9140
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    27
end;
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    28
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    29
structure IsarOutput: ISAR_OUTPUT =
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    30
struct
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    31
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    32
structure T = OuterLex;
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    33
structure P = OuterParse;
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    34
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    35
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    36
(** maintain global commands **)
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    37
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    38
local
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    39
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    40
val global_commands =
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    41
  ref (Symtab.empty: (Args.src -> Proof.context -> string) Symtab.table);
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    42
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    43
val global_options =
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    44
  ref (Symtab.empty: (string -> (unit -> string) -> unit -> string) Symtab.table);
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    45
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    46
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    47
fun add_item kind (tab, (name, x)) =
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    48
 (if is_none (Symtab.lookup (tab, name)) then ()
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    49
  else warning ("Redefined antiquotation output " ^ kind ^ ": " ^ quote name);
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    50
  Symtab.update ((name, x), tab));
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    51
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    52
fun add_items kind xs tab = foldl (add_item kind) (tab, xs);
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    53
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    54
in
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    55
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    56
val add_commands = Library.change global_commands o (add_items "command");
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    57
val add_options = Library.change global_options o (add_items "option");
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    58
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    59
fun command src =
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    60
  let val ((name, _), pos) = Args.dest_src src in
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    61
    (case Symtab.lookup (! global_commands, name) of
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    62
      None => error ("Unknown antiquotation command: " ^ quote name ^ Position.str_of pos)
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    63
    | Some f => transform_failure (curry Comment.OUTPUT_FAIL (name, pos)) (f src))
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    64
  end;
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    65
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    66
fun option (name, s) f () =
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    67
  (case Symtab.lookup (! global_options, name) of
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    68
    None => error ("Unknown antiquotation option: " ^ quote name)
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    69
  | Some opt => opt s f ());
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    70
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    71
fun options [] f = f
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    72
  | options (opt :: opts) f = option opt (options opts f);
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    73
9213
2651a4db8883 help_antiquotations;
wenzelm
parents: 9140
diff changeset
    74
9220
d0506ced27c8 added options "eta_contract", "long_names";
wenzelm
parents: 9213
diff changeset
    75
fun print_antiquotations () =
d0506ced27c8 added options "eta_contract", "long_names";
wenzelm
parents: 9213
diff changeset
    76
 [Pretty.big_list "antiquotation commands:" (map Pretty.str (Symtab.keys (! global_commands))),
d0506ced27c8 added options "eta_contract", "long_names";
wenzelm
parents: 9213
diff changeset
    77
  Pretty.big_list "antiquotation options:" (map Pretty.str (Symtab.keys (! global_options)))]
d0506ced27c8 added options "eta_contract", "long_names";
wenzelm
parents: 9213
diff changeset
    78
 |> Pretty.chunks |> Pretty.writeln;
9213
2651a4db8883 help_antiquotations;
wenzelm
parents: 9140
diff changeset
    79
9140
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    80
end;
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    81
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    82
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    83
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    84
(** syntax of antiquotations **)
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    85
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    86
(* option values *)
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    87
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    88
fun boolean "" = true
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    89
  | boolean "true" = true
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    90
  | boolean "false" = false
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    91
  | boolean s = error ("Bad boolean value: " ^ quote s);
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    92
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    93
fun integer s =
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    94
  let
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    95
    fun int ss =
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    96
      (case Term.read_int ss of (i, []) => i | _ => error ("Bad integer value: " ^ quote s));
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    97
  in (case Symbol.explode s of "-" :: ss => ~ (int ss) | ss => int ss) end;
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    98
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
    99
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   100
(* args syntax *)
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   101
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   102
fun syntax (scan: (Proof.context * Args.T list -> 'a * (Proof.context * Args.T list))) =
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   103
  Args.syntax "antiquotation" scan;
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   104
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   105
fun args scan f src ctxt : string =
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   106
  let val (ctxt', x) = syntax scan src ctxt
9750
270cd9831e7b added "source" option;
wenzelm
parents: 9732
diff changeset
   107
  in f src ctxt' x end;
9140
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   108
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   109
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   110
(* outer syntax *)
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   111
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   112
local
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   113
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   114
val property = P.xname -- Scan.optional (P.$$$ "=" |-- P.!!! P.xname) "";
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   115
val properties = Scan.optional (P.$$$ "[" |-- P.!!! (P.enum "," property --| P.$$$ "]")) [];
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   116
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   117
val antiq = P.position P.xname -- properties -- P.arguments --| Scan.ahead P.eof
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   118
  >> (fn (((x, pos), y), z) => (y, Args.src ((x, z), pos)));
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   119
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   120
fun antiq_args_aux keyword_lexicon (str, pos) =
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   121
  Source.of_string str
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   122
  |> Symbol.source false
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   123
  |> T.source false (K (keyword_lexicon, Scan.empty_lexicon)) pos
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   124
  |> T.source_proper
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   125
  |> Source.source T.stopper (Scan.error (Scan.bulk (P.!!! antiq))) None
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   126
  |> Source.exhaust;
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   127
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   128
in
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   129
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   130
fun antiq_args lex (s, pos) =
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   131
  (case antiq_args_aux lex (s, pos) of [x] => x | _ => raise ERROR) handle ERROR =>
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   132
    error ("Malformed antiquotation: " ^ quote ("@{" ^ s ^ "}") ^ Position.str_of pos);
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   133
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   134
end;
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   135
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   136
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   137
(* eval_antiquote *)
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   138
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   139
fun eval_antiquote lex state (str, pos) =
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   140
  let
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   141
    fun expand (Antiquote.Text s) = s
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   142
      | expand (Antiquote.Antiq x) =
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   143
          let val (opts, src) = antiq_args lex x in
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   144
            Library.setmp print_mode Latex.modes   (*note: lazy lookup of context below!*)
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   145
              (options opts (fn () => command src (Toplevel.context_of state))) () end;
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   146
    val ants = Antiquote.antiquotes_of (str, pos);
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   147
  in
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   148
    if Toplevel.is_toplevel state andalso exists Antiquote.is_antiq ants then
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   149
      error ("Cannot expand antiquotations at top-level" ^ Position.str_of pos)
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   150
    else implode (map expand ants)
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   151
  end;
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   152
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   153
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   154
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   155
(** present theory source **)
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   156
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   157
(* present_tokens *)
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   158
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   159
val interest_level = ref 0;
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   160
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   161
fun present_tokens lex toks state =
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   162
  toks
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   163
  |> mapfilter (fn (tk, i) => if i > ! interest_level then None else Some tk)
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   164
  |> map (apsnd (eval_antiquote lex state))
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   165
  |> Latex.output_tokens
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   166
  |> Buffer.add;
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   167
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   168
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   169
(* parse_thy *)
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   170
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   171
datatype markup = Markup | MarkupEnv | Verbatim;
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   172
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   173
local
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   174
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   175
val opt_newline = Scan.option (Scan.one T.is_newline);
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   176
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   177
fun check_level i =
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   178
  if i > 0 then Scan.succeed ()
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   179
  else Scan.fail_with (K "Bad nesting of meta-comments");
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   180
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   181
val ignore =
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   182
  Scan.depend (fn i => opt_newline |-- P.position (Scan.one T.is_begin_ignore) >> pair (i + 1)) ||
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   183
  Scan.depend (fn i => P.position (Scan.one T.is_end_ignore) --|
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   184
    (opt_newline -- check_level i) >> pair (i - 1));
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   185
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   186
val ignore_cmd = Scan.state -- ignore
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   187
  >> (fn (i, (x, pos)) => (false, ((Latex.Basic x, ("", pos)), i)));
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   188
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   189
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   190
val is_improper = not o (T.is_proper orf T.is_begin_ignore orf T.is_end_ignore);
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   191
val improper = Scan.any is_improper;
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   192
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   193
val improper_keep_indent = Scan.repeat
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   194
  (Scan.unless (Scan.one T.is_indent -- Scan.one T.is_proper) (Scan.one is_improper));
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   195
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   196
val improper_end =
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   197
  (improper -- P.semicolon) |-- improper_keep_indent ||
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   198
  improper_keep_indent;
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   199
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   200
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   201
val stopper =
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   202
  ((false, ((Latex.Basic (#1 T.stopper), ("", Position.none)), 0)),
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   203
    fn (_, ((Latex.Basic x, _), _)) => (#2 T.stopper x) | _ => false);
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   204
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   205
in
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   206
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   207
fun parse_thy markup lex trs src =
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   208
  let
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   209
    val text = P.position P.text;
9220
d0506ced27c8 added options "eta_contract", "long_names";
wenzelm
parents: 9213
diff changeset
   210
    val token = Scan.depend (fn i =>
9140
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   211
     (improper |-- markup Markup -- P.!!!! (improper |-- text --| improper_end)
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   212
        >> (fn (x, y) => (true, ((Latex.Markup (T.val_of x), y), i))) ||
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   213
      improper |-- markup MarkupEnv -- P.!!!! (improper |-- text --| improper_end)
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   214
        >> (fn (x, y) => (true, ((Latex.MarkupEnv (T.val_of x), y), i))) ||
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   215
      (P.$$$ "--" |-- P.!!!! (improper |-- text))
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   216
        >> (fn y => (false, ((Latex.Markup "cmt", y), i))) ||
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   217
      (improper -- markup Verbatim) |-- P.!!!! (improper |-- text --| improper_end)
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   218
        >> (fn y => (true, ((Latex.Verbatim, y), i))) ||
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   219
      P.position (Scan.one T.not_eof)
9220
d0506ced27c8 added options "eta_contract", "long_names";
wenzelm
parents: 9213
diff changeset
   220
        >> (fn (x, pos) => (T.is_kind T.Command x, ((Latex.Basic x, ("", pos)), i))))
d0506ced27c8 added options "eta_contract", "long_names";
wenzelm
parents: 9213
diff changeset
   221
      >> pair i);
9140
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   222
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   223
    val body = Scan.any (not o fst andf not o #2 stopper);
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   224
    val section = body -- Scan.one fst -- body >> (fn ((x, y), z) => map snd (x @ (y :: z)));
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   225
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   226
    val cmds =
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   227
      src
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   228
      |> Source.filter (not o T.is_semicolon)
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   229
      |> Source.source' 0 T.stopper (Scan.error (Scan.bulk (ignore_cmd || token))) None
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   230
      |> Source.source stopper (Scan.error (Scan.bulk section)) None
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   231
      |> Source.exhaust;
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   232
  in
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   233
    if length cmds = length trs then
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   234
      (trs ~~ map (present_tokens lex) cmds, Buffer.empty)
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   235
    else error "Messed up outer syntax for presentation"
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   236
  end;
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   237
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   238
end;
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   239
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   240
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   241
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   242
(** setup default output **)
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   243
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   244
(* options *)
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   245
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   246
val display = ref false;
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   247
val quotes = ref false;
9732
c32c7ef228c6 added "name" antiq and "indent" option;
wenzelm
parents: 9504
diff changeset
   248
val indent = ref 0;
9750
270cd9831e7b added "source" option;
wenzelm
parents: 9732
diff changeset
   249
val source = ref false;
9140
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   250
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   251
val _ = add_options
9220
d0506ced27c8 added options "eta_contract", "long_names";
wenzelm
parents: 9213
diff changeset
   252
 [("show_types", Library.setmp Syntax.show_types o boolean),
d0506ced27c8 added options "eta_contract", "long_names";
wenzelm
parents: 9213
diff changeset
   253
  ("show_sorts", Library.setmp Syntax.show_sorts o boolean),
d0506ced27c8 added options "eta_contract", "long_names";
wenzelm
parents: 9213
diff changeset
   254
  ("eta_contract", Library.setmp Syntax.eta_contract o boolean),
d0506ced27c8 added options "eta_contract", "long_names";
wenzelm
parents: 9213
diff changeset
   255
  ("long_names", Library.setmp NameSpace.long_names o boolean),
9140
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   256
  ("display", Library.setmp display o boolean),
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   257
  ("quotes", Library.setmp quotes o boolean),
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   258
  ("mode", fn s => fn f => fn () => Library.setmp print_mode (s :: ! print_mode) f ()),
9732
c32c7ef228c6 added "name" antiq and "indent" option;
wenzelm
parents: 9504
diff changeset
   259
  ("margin", Pretty.setmp_margin o integer),
9750
270cd9831e7b added "source" option;
wenzelm
parents: 9732
diff changeset
   260
  ("indent", Library.setmp indent o integer),
270cd9831e7b added "source" option;
wenzelm
parents: 9732
diff changeset
   261
  ("source", Library.setmp source o boolean)];
9140
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   262
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   263
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   264
(* commands *)
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   265
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   266
local
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   267
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   268
fun cond_quote prt =
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   269
  if ! quotes then Pretty.quote prt else prt;
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   270
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   271
fun cond_display prt =
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   272
  if ! display then
9732
c32c7ef228c6 added "name" antiq and "indent" option;
wenzelm
parents: 9504
diff changeset
   273
    Pretty.string_of (Pretty.indent (! indent) prt)
9828
1d8bc4f1833e display: avoid empty lines;
wenzelm
parents: 9750
diff changeset
   274
    |> enclose "%\n\\begin{isabelle}%\n" "%\n\\end{isabelle}%\n"
9140
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   275
  else
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   276
    Pretty.str_of prt
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   277
    |> enclose "\\isa{" "}";
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   278
9750
270cd9831e7b added "source" option;
wenzelm
parents: 9732
diff changeset
   279
270cd9831e7b added "source" option;
wenzelm
parents: 9732
diff changeset
   280
val pretty_text = Pretty.chunks o map Pretty.str o Library.split_lines;
9140
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   281
9750
270cd9831e7b added "source" option;
wenzelm
parents: 9732
diff changeset
   282
val pretty_source =
270cd9831e7b added "source" option;
wenzelm
parents: 9732
diff changeset
   283
  pretty_text o space_implode " " o map Args.string_of o #2 o #1 o Args.dest_src;
9140
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   284
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   285
fun pretty_typ ctxt T =
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   286
  Sign.pretty_typ (ProofContext.sign_of ctxt) T;
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   287
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   288
fun pretty_term ctxt t =
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   289
  Sign.pretty_term (ProofContext.sign_of ctxt) (ProofContext.extern_skolem ctxt t);
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   290
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   291
fun pretty_thm ctxt thms =
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   292
  Pretty.chunks (map (pretty_term ctxt o #prop o Thm.rep_thm) thms);
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   293
9750
270cd9831e7b added "source" option;
wenzelm
parents: 9732
diff changeset
   294
270cd9831e7b added "source" option;
wenzelm
parents: 9732
diff changeset
   295
fun output_with pretty src ctxt x =
270cd9831e7b added "source" option;
wenzelm
parents: 9732
diff changeset
   296
  let
270cd9831e7b added "source" option;
wenzelm
parents: 9732
diff changeset
   297
    val prt = pretty ctxt x;      (*always pretty!*)
270cd9831e7b added "source" option;
wenzelm
parents: 9732
diff changeset
   298
    val prt' = if ! source then pretty_source src else prt;
270cd9831e7b added "source" option;
wenzelm
parents: 9732
diff changeset
   299
  in cond_display (cond_quote prt') end;
9732
c32c7ef228c6 added "name" antiq and "indent" option;
wenzelm
parents: 9504
diff changeset
   300
9140
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   301
in
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   302
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   303
val _ = add_commands
9750
270cd9831e7b added "source" option;
wenzelm
parents: 9732
diff changeset
   304
 [("text", args (Scan.lift Args.name) (output_with (K pretty_text))),
270cd9831e7b added "source" option;
wenzelm
parents: 9732
diff changeset
   305
  ("thm", args Attrib.local_thms (output_with pretty_thm)),
270cd9831e7b added "source" option;
wenzelm
parents: 9732
diff changeset
   306
  ("prop", args Args.local_prop (output_with pretty_term)),
270cd9831e7b added "source" option;
wenzelm
parents: 9732
diff changeset
   307
  ("term", args Args.local_term (output_with pretty_term)),
270cd9831e7b added "source" option;
wenzelm
parents: 9732
diff changeset
   308
  ("typ", args Args.local_typ_no_norm (output_with pretty_typ))];
9140
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   309
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   310
end;
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   311
69e8938c2409 Isar theory output.
wenzelm
parents:
diff changeset
   312
end;