# HG changeset patch
# User wenzelm
# Date 1236617633 -3600
# Node ID ad591ee76c78160ab0e5fdd7df0466c42f321d5e
# Parent  85c7ffbfac17bdb484a958998959a877e1806812
simplified interface to define document antiquotations, cf. antiquotatation, maybe_pretty_source, output;
removed incomprehensible args parser setup;
removed obsolete locale flag -- text is already localized;
misc tuning and cleanup of concrete antiquotations;
goal state antiquotations: ignore source flag;

diff -r 85c7ffbfac17 -r ad591ee76c78 src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Mon Mar 09 15:49:55 2009 +0100
+++ b/src/Pure/Thy/thy_output.ML	Mon Mar 09 17:53:53 2009 +0100
@@ -1,7 +1,7 @@
 (*  Title:      Pure/Thy/thy_output.ML
     Author:     Markus Wenzel, TU Muenchen
 
-Theory document output.
+Theory document output with antiquotations.
 *)
 
 signature THY_OUTPUT =
@@ -21,20 +21,17 @@
   val antiquotation: string ->
     (Context.generic * Args.T list -> 'a * (Context.generic * Args.T list)) ->
     ({state: Toplevel.state, source: Args.src, context: Proof.context} -> 'a -> string) -> unit
-  val args: (Context.generic * Args.T list -> 'a * (Context.generic * Args.T list)) ->
-    (Args.src -> Proof.context -> 'a -> string) -> Args.src -> Toplevel.state -> string
   datatype markup = Markup | MarkupEnv | Verbatim
   val modes: string list ref
   val eval_antiquote: Scan.lexicon -> Toplevel.state -> SymbolPos.text * Position.T -> string
   val present_thy: Scan.lexicon -> (string -> string list) -> (markup -> string -> bool) ->
     (Toplevel.transition * Toplevel.state) list -> (OuterLex.token, 'a) Source.source -> Buffer.T
-  val str_of_source: Args.src -> string
   val pretty_text: string -> Pretty.T
   val pretty_term: Proof.context -> term -> Pretty.T
   val pretty_thm: Proof.context -> thm -> Pretty.T
-  val output_list: (Proof.context -> 'a -> Pretty.T) -> Args.src ->
-    Proof.context -> 'a list -> string
-  val output: (Proof.context -> 'a -> Pretty.T) -> Args.src -> Proof.context -> 'a -> string
+  val str_of_source: Args.src -> string
+  val maybe_pretty_source: ('a -> Pretty.T) -> Args.src -> 'a list -> Pretty.T list
+  val output: Pretty.T list -> string
 end;
 
 structure ThyOutput: THY_OUTPUT =
@@ -46,7 +43,6 @@
 
 (** global options **)
 
-val locale = ref "";
 val display = ref false;
 val quotes = ref false;
 val indent = ref 0;
@@ -55,7 +51,7 @@
 
 
 
-(** maintain global commands **)
+(** maintain global antiquotations **)
 
 local
 
@@ -107,6 +103,11 @@
 
 end;
 
+fun antiquotation name scan out = add_commands [(name, fn src => fn state =>
+  let val (x, ctxt) = Args.context_syntax "document antiquotation"
+    scan src (Toplevel.presentation_context_of state NONE)
+  in out {source = src, state = state, context = ctxt} x end)];
+
 
 
 (** syntax of antiquotations **)
@@ -126,22 +127,6 @@
   in (case Symbol.explode s of "-" :: ss => ~ (int ss) | ss => int ss) end;
 
 
-(* args syntax *)
-
-fun syntax scan = Args.context_syntax "document antiquotation" scan;
-
-fun antiquotation name scan output =
-  add_commands [(name, fn src => fn state =>
-    let val (x, ctxt) = syntax scan src (Toplevel.presentation_context_of state NONE);
-    in output {source = src, state = state, context = ctxt} x end)];
-
-fun args scan f src state : string =
-  let
-    val loc = if ! locale = "" then NONE else SOME (! locale);
-    val (x, ctxt) = syntax scan src (Toplevel.presentation_context_of state loc);
-  in f src ctxt x end;
-
-
 (* outer syntax *)
 
 local
@@ -438,7 +423,6 @@
   ("short_names", Library.setmp NameSpace.short_names o boolean),
   ("unique_names", Library.setmp NameSpace.unique_names o boolean),
   ("eta_contract", Library.setmp Syntax.eta_contract o boolean),
-  ("locale", Library.setmp locale),
   ("display", Library.setmp display o boolean),
   ("break", Library.setmp break o boolean),
   ("quotes", Library.setmp quotes o boolean),
@@ -451,8 +435,6 @@
 
 (* basic pretty printing *)
 
-val str_of_source = space_implode " " o map T.unparse o #2 o #1 o Args.dest_src;
-
 fun tweak_line s =
   if ! display then s else Symbol.strip_blanks s;
 
@@ -493,18 +475,22 @@
 fun pretty_thm_style ctxt (name, th) =
   pretty_term_style ctxt (name, Thm.full_prop_of th);
 
-fun pretty_prf full ctxt thms =
-  Pretty.chunks (map (ProofSyntax.pretty_proof_of ctxt full) thms);
+fun pretty_prf full ctxt = ProofSyntax.pretty_proof_of ctxt full;
 
 fun pretty_theory ctxt name =
   (Theory.requires (ProofContext.theory_of ctxt) name "presentation"; Pretty.str name);
 
 
-(* Isar output *)
+(* default output *)
+
+val str_of_source = space_implode " " o map T.unparse o #2 o #1 o Args.dest_src;
 
-fun output_list pretty src ctxt xs =
-  map (pretty ctxt) xs        (*always pretty in order to exhibit errors!*)
-  |> (if ! source then K [pretty_text (str_of_source src)] else I)
+fun maybe_pretty_source pretty src xs =
+  map pretty xs  (*always pretty in order to exhibit errors!*)
+  |> (if ! source then K [pretty_text (str_of_source src)] else I);
+
+fun output prts =
+  prts
   |> (if ! quotes then map Pretty.quote else I)
   |> (if ! display then
     map (Output.output o Pretty.string_of o Pretty.indent (! indent))
@@ -515,69 +501,98 @@
     #> space_implode "\\isasep\\isanewline%\n"
     #> enclose "\\isa{" "}");
 
-fun output pretty src ctxt = output_list pretty src ctxt o single;
+
+
+(** concrete antiquotations **)
+
+(* basic entities *)
+
+local
+
+fun basic_entities name scan pretty = antiquotation name scan
+  (fn {source, context, ...} => output o maybe_pretty_source (pretty context) source);
+
+fun basic_entity name scan = basic_entities name (scan >> single);
+
+in
+
+val _ = basic_entities "thm" Attrib.thms pretty_thm;
+val _ = basic_entity "thm_style" (Scan.lift Args.liberal_name -- Attrib.thm) pretty_thm_style;
+val _ = basic_entity "prop" Args.prop pretty_term;
+val _ = basic_entity "term" Args.term pretty_term;
+val _ = basic_entity "term_style" (Scan.lift Args.liberal_name -- Args.term) pretty_term_style;
+val _ = basic_entity "term_type" Args.term pretty_term_typ;
+val _ = basic_entity "typeof" Args.term pretty_term_typeof;
+val _ = basic_entity "const" Args.const_proper pretty_const;
+val _ = basic_entity "abbrev" (Scan.lift Args.name_source) pretty_abbrev;
+val _ = basic_entity "typ" Args.typ_abbrev Syntax.pretty_typ;
+val _ = basic_entity "text" (Scan.lift Args.name) (K pretty_text);
+val _ = basic_entities "prf" Attrib.thms (pretty_prf false);
+val _ = basic_entities "full_prf" Attrib.thms (pretty_prf true);
+val _ = basic_entity "theory" (Scan.lift Args.name) pretty_theory;
+
+end;
+
+
+(* goal state *)
+
+local
 
 fun proof_state state =
   (case try Toplevel.proof_of state of
     SOME prf => prf
   | _ => error "No proof state");
 
-fun output_goals main_goal src state = args (Scan.succeed ()) (output (fn _ => fn _ =>
-  Pretty.chunks (Proof.pretty_goals main_goal (proof_state state)))) src state;
-
-fun ml_val txt = "fn _ => (" ^ txt ^ ");";
-fun ml_type txt = "val _ = NONE : (" ^ txt ^ ") option;";
-fun ml_struct txt = "functor DUMMY_FUNCTOR() = struct structure DUMMY = " ^ txt ^ " end;"
+fun goal_state name main_goal = antiquotation name (Scan.succeed ())
+  (fn {state, ...} => fn () => output
+    [Pretty.chunks (Proof.pretty_goals main_goal (proof_state state))]);
 
-fun output_ml ml _ ctxt (txt, pos) =
- (ML_Context.eval_in (SOME ctxt) false pos (ml txt);
-  SymbolPos.content (SymbolPos.explode (txt, pos))
-  |> (if ! quotes then quote else I)
-  |> (if ! display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
-  else
-    split_lines
-    #> map (space_implode "\\verb,|," o map (enclose "\\verb|" "|") o space_explode "|")
-    #> space_implode "\\isasep\\isanewline%\n"));
+in
+
+val _ = goal_state "goals" true;
+val _ = goal_state "subgoals" false;
+
+end;
 
 
-(* embedded lemmas *)
-
-fun pretty_lemma ctxt (prop, methods) =
-  let
-    val _ = ctxt
-      |> Proof.theorem_i NONE (K I) [[(prop, [])]]
-      |> Proof.global_terminal_proof methods;
-  in pretty_term ctxt prop end;
-
-val embedded_lemma =
-  args (Args.prop -- Scan.lift (Args.$$$ "by" |-- Method.parse -- Scan.option Method.parse))
-    (output pretty_lemma o (fn ((a, arg :: _), p) => (Args.src ((a, [arg]), p))) o Args.dest_src);
-
-
-(* commands *)
+(* embedded lemma *)
 
 val _ = OuterKeyword.keyword "by";
 
-val _ = add_commands
- [("thm", args Attrib.thms (output_list pretty_thm)),
-  ("thm_style", args (Scan.lift Args.liberal_name -- Attrib.thm) (output pretty_thm_style)),
-  ("prop", args Args.prop (output pretty_term)),
-  ("lemma", embedded_lemma),
-  ("term", args Args.term (output pretty_term)),
-  ("term_style", args (Scan.lift Args.liberal_name -- Args.term) (output pretty_term_style)),
-  ("term_type", args Args.term (output pretty_term_typ)),
-  ("typeof", args Args.term (output pretty_term_typeof)),
-  ("const", args Args.const_proper (output pretty_const)),
-  ("abbrev", args (Scan.lift Args.name_source) (output pretty_abbrev)),
-  ("typ", args Args.typ_abbrev (output Syntax.pretty_typ)),
-  ("text", args (Scan.lift Args.name) (output (K pretty_text))),
-  ("goals", output_goals true),
-  ("subgoals", output_goals false),
-  ("prf", args Attrib.thms (output (pretty_prf false))),
-  ("full_prf", args Attrib.thms (output (pretty_prf true))),
-  ("theory", args (Scan.lift Args.name) (output pretty_theory)),
-  ("ML", args (Scan.lift Args.name_source_position) (output_ml ml_val)),
-  ("ML_type", args (Scan.lift Args.name_source_position) (output_ml ml_type)),
-  ("ML_struct", args (Scan.lift Args.name_source_position) (output_ml ml_struct))];
+val _ = antiquotation "lemma"
+  (Args.prop -- Scan.lift (Args.$$$ "by" |-- Method.parse -- Scan.option Method.parse))
+  (fn {source, context, ...} => fn (prop, methods) =>
+    let
+      val prop_src =
+        (case Args.dest_src source of ((a, arg :: _), pos) => Args.src ((a, [arg]), pos));
+      val _ = context
+        |> Proof.theorem_i NONE (K I) [[(prop, [])]]
+        |> Proof.global_terminal_proof methods;
+    in output (maybe_pretty_source (pretty_term context) prop_src [prop]) end);
+
+
+(* ML text *)
+
+local
+
+fun ml_text name ml = antiquotation name (Scan.lift Args.name_source_position)
+  (fn {context, ...} => fn (txt, pos) =>
+   (ML_Context.eval_in (SOME context) false pos (ml txt);
+    SymbolPos.content (SymbolPos.explode (txt, pos))
+    |> (if ! quotes then quote else I)
+    |> (if ! display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
+    else
+      split_lines
+      #> map (space_implode "\\verb,|," o map (enclose "\\verb|" "|") o space_explode "|")
+      #> space_implode "\\isasep\\isanewline%\n")));
+
+in
+
+val _ = ml_text "ML" (fn txt => "fn _ => (" ^ txt ^ ");");
+val _ = ml_text "ML_type" (fn txt => "val _ = NONE : (" ^ txt ^ ") option;");
+val _ = ml_text "ML_struct"
+  (fn txt => "functor DUMMY_FUNCTOR() = struct structure DUMMY = " ^ txt ^ " end;");
 
 end;
+
+end;