# HG changeset patch # User wenzelm # Date 961970249 -7200 # Node ID 69e8938c24090675d6756a0bdeaf6a423c7e7b1d # Parent bf272b4985ec031b33efb4f679084812fa867c46 Isar theory output. diff -r bf272b4985ec -r 69e8938c2409 src/Pure/Isar/isar_output.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/Isar/isar_output.ML Sun Jun 25 23:57:29 2000 +0200 @@ -0,0 +1,286 @@ +(* Title: Pure/Isar/isar_output.ML + ID: $Id$ + Author: Markus Wenzel, TU Muenchen + License: GPL (GNU GENERAL PUBLIC LICENSE) + +Isar theory output. +*) + +signature ISAR_OUTPUT = +sig + val add_commands: (string * (Args.src -> Proof.context -> string)) list -> unit + val add_options: (string * (string -> (unit -> string) -> unit -> string)) list -> unit + val boolean: string -> bool + val integer: string -> int + val args: (Proof.context * Args.T list -> 'a * (Proof.context * Args.T list)) -> + (Proof.context -> 'a -> string) -> Args.src -> Proof.context -> string + datatype markup = Markup | MarkupEnv | Verbatim + val interest_level: int ref + val parse_thy: (markup -> OuterLex.token list -> OuterLex.token * OuterLex.token list) -> + Scan.lexicon -> Toplevel.transition list -> (OuterLex.token, 'a) Source.source -> + (Toplevel.transition * (Toplevel.state -> Buffer.T -> Buffer.T)) list * Buffer.T + val display: bool ref + val quotes: bool ref +end; + +structure IsarOutput: ISAR_OUTPUT = +struct + +structure T = OuterLex; +structure P = OuterParse; + + +(** maintain global commands **) + +local + +val global_commands = + ref (Symtab.empty: (Args.src -> Proof.context -> string) Symtab.table); + +val global_options = + ref (Symtab.empty: (string -> (unit -> string) -> unit -> string) Symtab.table); + + +fun add_item kind (tab, (name, x)) = + (if is_none (Symtab.lookup (tab, name)) then () + else warning ("Redefined antiquotation output " ^ kind ^ ": " ^ quote name); + Symtab.update ((name, x), tab)); + +fun add_items kind xs tab = foldl (add_item kind) (tab, xs); + +in + +val add_commands = Library.change global_commands o (add_items "command"); +val add_options = Library.change global_options o (add_items "option"); + +fun command src = + let val ((name, _), pos) = Args.dest_src src in + (case Symtab.lookup (! global_commands, name) of + None => error ("Unknown antiquotation command: " ^ quote name ^ Position.str_of pos) + | Some f => transform_failure (curry Comment.OUTPUT_FAIL (name, pos)) (f src)) + end; + +fun option (name, s) f () = + (case Symtab.lookup (! global_options, name) of + None => error ("Unknown antiquotation option: " ^ quote name) + | Some opt => opt s f ()); + +fun options [] f = f + | options (opt :: opts) f = option opt (options opts f); + +end; + + + +(** syntax of antiquotations **) + +(* option values *) + +fun boolean "" = true + | boolean "true" = true + | boolean "false" = false + | boolean s = error ("Bad boolean value: " ^ quote s); + +fun integer s = + let + fun int ss = + (case Term.read_int ss of (i, []) => i | _ => error ("Bad integer value: " ^ quote s)); + in (case Symbol.explode s of "-" :: ss => ~ (int ss) | ss => int ss) end; + + +(* args syntax *) + +fun syntax (scan: (Proof.context * Args.T list -> 'a * (Proof.context * Args.T list))) = + Args.syntax "antiquotation" scan; + +fun args scan f src ctxt : string = + let val (ctxt', x) = syntax scan src ctxt + in f ctxt' x end; + + +(* outer syntax *) + +local + +val property = P.xname -- Scan.optional (P.$$$ "=" |-- P.!!! P.xname) ""; +val properties = Scan.optional (P.$$$ "[" |-- P.!!! (P.enum "," property --| P.$$$ "]")) []; + +val antiq = P.position P.xname -- properties -- P.arguments --| Scan.ahead P.eof + >> (fn (((x, pos), y), z) => (y, Args.src ((x, z), pos))); + +fun antiq_args_aux keyword_lexicon (str, pos) = + Source.of_string str + |> Symbol.source false + |> T.source false (K (keyword_lexicon, Scan.empty_lexicon)) pos + |> T.source_proper + |> Source.source T.stopper (Scan.error (Scan.bulk (P.!!! antiq))) None + |> Source.exhaust; + +in + +fun antiq_args lex (s, pos) = + (case antiq_args_aux lex (s, pos) of [x] => x | _ => raise ERROR) handle ERROR => + error ("Malformed antiquotation: " ^ quote ("@{" ^ s ^ "}") ^ Position.str_of pos); + +end; + + +(* eval_antiquote *) + +fun eval_antiquote lex state (str, pos) = + let + fun expand (Antiquote.Text s) = s + | expand (Antiquote.Antiq x) = + let val (opts, src) = antiq_args lex x in + Library.setmp print_mode Latex.modes (*note: lazy lookup of context below!*) + (options opts (fn () => command src (Toplevel.context_of state))) () end; + val ants = Antiquote.antiquotes_of (str, pos); + in + if Toplevel.is_toplevel state andalso exists Antiquote.is_antiq ants then + error ("Cannot expand antiquotations at top-level" ^ Position.str_of pos) + else implode (map expand ants) + end; + + + +(** present theory source **) + +(* present_tokens *) + +val interest_level = ref 0; + +fun present_tokens lex toks state = + toks + |> mapfilter (fn (tk, i) => if i > ! interest_level then None else Some tk) + |> map (apsnd (eval_antiquote lex state)) + |> Latex.output_tokens + |> Buffer.add; + + +(* parse_thy *) + +datatype markup = Markup | MarkupEnv | Verbatim; + +local + +val opt_newline = Scan.option (Scan.one T.is_newline); + +fun check_level i = + if i > 0 then Scan.succeed () + else Scan.fail_with (K "Bad nesting of meta-comments"); + +val ignore = + Scan.depend (fn i => opt_newline |-- P.position (Scan.one T.is_begin_ignore) >> pair (i + 1)) || + Scan.depend (fn i => P.position (Scan.one T.is_end_ignore) --| + (opt_newline -- check_level i) >> pair (i - 1)); + +val ignore_cmd = Scan.state -- ignore + >> (fn (i, (x, pos)) => (false, ((Latex.Basic x, ("", pos)), i))); + + +val is_improper = not o (T.is_proper orf T.is_begin_ignore orf T.is_end_ignore); +val improper = Scan.any is_improper; + +val improper_keep_indent = Scan.repeat + (Scan.unless (Scan.one T.is_indent -- Scan.one T.is_proper) (Scan.one is_improper)); + +val improper_end = + (improper -- P.semicolon) |-- improper_keep_indent || + improper_keep_indent; + + +val stopper = + ((false, ((Latex.Basic (#1 T.stopper), ("", Position.none)), 0)), + fn (_, ((Latex.Basic x, _), _)) => (#2 T.stopper x) | _ => false); + +in + +fun parse_thy markup lex trs src = + let + val text = P.position P.text; + val token = Scan.state :-- (fn i => Scan.lift + (improper |-- markup Markup -- P.!!!! (improper |-- text --| improper_end) + >> (fn (x, y) => (true, ((Latex.Markup (T.val_of x), y), i))) || + improper |-- markup MarkupEnv -- P.!!!! (improper |-- text --| improper_end) + >> (fn (x, y) => (true, ((Latex.MarkupEnv (T.val_of x), y), i))) || + (P.$$$ "--" |-- P.!!!! (improper |-- text)) + >> (fn y => (false, ((Latex.Markup "cmt", y), i))) || + (improper -- markup Verbatim) |-- P.!!!! (improper |-- text --| improper_end) + >> (fn y => (true, ((Latex.Verbatim, y), i))) || + P.position (Scan.one T.not_eof) + >> (fn (x, pos) => (T.is_kind T.Command x, ((Latex.Basic x, ("", pos)), i))))) + >> #2; + + val body = Scan.any (not o fst andf not o #2 stopper); + val section = body -- Scan.one fst -- body >> (fn ((x, y), z) => map snd (x @ (y :: z))); + + val cmds = + src + |> Source.filter (not o T.is_semicolon) + |> Source.source' 0 T.stopper (Scan.error (Scan.bulk (ignore_cmd || token))) None + |> Source.source stopper (Scan.error (Scan.bulk section)) None + |> Source.exhaust; + in + if length cmds = length trs then + (trs ~~ map (present_tokens lex) cmds, Buffer.empty) + else error "Messed up outer syntax for presentation" + end; + +end; + + + +(** setup default output **) + +(* options *) + +val display = ref false; +val quotes = ref false; + +val _ = add_options + [("show_types", Library.setmp show_types o boolean), + ("show_sorts", Library.setmp show_sorts o boolean), + ("display", Library.setmp display o boolean), + ("quotes", Library.setmp quotes o boolean), + ("mode", fn s => fn f => fn () => Library.setmp print_mode (s :: ! print_mode) f ()), + ("margin", Pretty.setmp_margin o integer)]; + + +(* commands *) + +local + +fun cond_quote prt = + if ! quotes then Pretty.quote prt else prt; + +fun cond_display prt = + if ! display then + Pretty.string_of prt + |> enclose "\n\\begin{isabelle}%\n" "\n\\end{isabelle}%\n" + else + Pretty.str_of prt + |> enclose "\\isa{" "}"; + +val string_of = cond_display o cond_quote; + + +fun pretty_typ ctxt T = + Sign.pretty_typ (ProofContext.sign_of ctxt) T; + +fun pretty_term ctxt t = + Sign.pretty_term (ProofContext.sign_of ctxt) (ProofContext.extern_skolem ctxt t); + +fun pretty_thm ctxt thms = + Pretty.chunks (map (pretty_term ctxt o #prop o Thm.rep_thm) thms); + +in + +val _ = add_commands + [("thm", args Attrib.local_thms (string_of oo pretty_thm)), + ("prop", args Args.local_prop (string_of oo pretty_term)), + ("term", args Args.local_term (string_of oo pretty_term)), + ("typ", args Args.local_typ (string_of oo pretty_typ))]; + +end; + +end;