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