--- a/NEWS Sun Jan 07 12:41:34 2018 +0100
+++ b/NEWS Sun Jan 07 13:45:21 2018 +0100
@@ -10,7 +10,8 @@
*** General ***
* Inner syntax comments may be written as "\<comment> \<open>text\<close>", similar to
-marginal comments in outer syntax.
+marginal comments in outer syntax: antiquotations are supported as usual
+(wrt. the overall command context).
* The old 'def' command has been discontinued (legacy since
Isbelle2016-1). INCOMPATIBILITY, use 'define' instead -- usually with
--- a/src/Pure/Thy/document_antiquotations.ML Sun Jan 07 12:41:34 2018 +0100
+++ b/src/Pure/Thy/document_antiquotations.ML Sun Jan 07 13:45:21 2018 +0100
@@ -84,7 +84,7 @@
val _ =
Theory.setup
(Thy_Output.antiquotation \<^binding>\<open>theory_text\<close> (Scan.lift Args.text_input)
- (fn {context = ctxt, ...} => fn source =>
+ (fn {state, context = ctxt, ...} => fn source =>
let
val _ =
Context_Position.report ctxt (Input.pos_of source)
@@ -101,7 +101,7 @@
val indentation =
Latex.output_symbols (replicate (Config.get ctxt Thy_Output.indent) Symbol.space);
in
- Latex.output_text (maps Thy_Output.output_token toks) |>
+ Latex.output_text (maps (Thy_Output.output_token state) toks) |>
(if Config.get ctxt Thy_Output.display then
split_lines #> map (prefix indentation) #> cat_lines #>
Latex.environment "isabelle"
--- a/src/Pure/Thy/thy_output.ML Sun Jan 07 12:41:34 2018 +0100
+++ b/src/Pure/Thy/thy_output.ML Sun Jan 07 13:45:21 2018 +0100
@@ -25,7 +25,7 @@
val integer: string -> int
val eval_antiquote: Toplevel.state -> Antiquote.text_antiquote -> string
val output_text: Toplevel.state -> {markdown: bool} -> Input.source -> Latex.text list
- val output_token: Token.T -> Latex.text list
+ val output_token: Toplevel.state -> Token.T -> Latex.text list
val present_thy: theory -> (Toplevel.transition * Toplevel.state) list ->
Token.T list -> Latex.text list
val pretty_text: Proof.context -> string -> Pretty.T
@@ -193,6 +193,9 @@
end;
+
+(** document output **)
+
(* output text *)
fun output_text state {markdown} source =
@@ -241,16 +244,29 @@
end;
-
-(** present theory source **)
+(* output tokens with comments *)
-(*NB: arranging white space around command spans is a black art*)
-
-
-(* Isar tokens *)
+fun output_markup state cmd source =
+ Latex.enclose_body ("%\n\\isamarkup" ^ cmd ^ "{") "%\n}\n"
+ (output_text state {markdown = false} source);
local
+fun output_symbols syms =
+ [Latex.text (Latex.output_symbols (map Symbol_Pos.symbol syms), #1 (Symbol_Pos.range syms))];
+
+fun output_symbols_comment state (is_comment, syms) =
+ if is_comment then
+ output_markup state "cmt"
+ (Input.source true (Symbol_Pos.implode syms) (Symbol_Pos.range syms))
+ else output_symbols syms;
+
+val scan_symbols_comment =
+ Scan.many1 (fn (s, _) => s <> Symbol.comment andalso Symbol.not_eof s) >> pair false ||
+ (Symbol_Pos.$$ Symbol.comment ::: Scan.many (Symbol.is_blank o Symbol_Pos.symbol)) --
+ Scan.option (Symbol_Pos.scan_cartouche_content "Document token error: ")
+ >> (fn (syms, NONE) => (false, syms) | (_, SOME syms) => (true, syms));
+
val output_syms_antiq =
(fn Antiquote.Text ss => Latex.output_symbols_pos ss
| Antiquote.Control {name = (name, _), body, ...} =>
@@ -261,33 +277,46 @@
in
-fun output_token tok =
+fun output_body state bg en syms =
+ (if exists (fn (s, _) => s = Symbol.comment) syms then
+ (case Scan.read Symbol_Pos.stopper (Scan.repeat scan_symbols_comment) syms of
+ SOME res => maps (output_symbols_comment state) res
+ | NONE => output_symbols syms)
+ else output_symbols syms) |> Latex.enclose_body bg en
+and output_token state tok =
let
- val s = Token.content_of tok;
+ val syms = Input.source_explode (Token.input_of tok);
val output =
- if Token.is_kind Token.Comment tok then ""
- else if Token.is_command tok then
- "\\isacommand{" ^ Latex.output_syms s ^ "}"
- else if Token.is_kind Token.Keyword tok andalso Symbol.is_ascii_identifier s then
- "\\isakeyword{" ^ Latex.output_syms s ^ "}"
+ if Token.is_kind Token.Comment tok then []
+ else if Token.is_command tok then output_body state "\\isacommand{" "}" syms
+ else if Token.is_kind Token.Keyword tok andalso
+ Symbol.is_ascii_identifier (Token.content_of tok)
+ then output_body state "\\isakeyword{" "}" syms
else if Token.is_kind Token.String tok then
- enclose "{\\isachardoublequoteopen}" "{\\isachardoublequoteclose}" (Latex.output_syms s)
+ output_body state "{\\isachardoublequoteopen}" "{\\isachardoublequoteclose}" syms
else if Token.is_kind Token.Alt_String tok then
- enclose "{\\isacharbackquoteopen}" "{\\isacharbackquoteclose}" (Latex.output_syms s)
+ output_body state "{\\isacharbackquoteopen}" "{\\isacharbackquoteclose}" syms
else if Token.is_kind Token.Verbatim tok then
let
+ val pos = Token.pos_of tok;
val ants = Antiquote.read (Token.input_of tok);
val out = implode (map output_syms_antiq ants);
- in enclose "{\\isacharverbatimopen}" "{\\isacharverbatimclose}" out end
+ in [Latex.text (enclose "{\\isacharverbatimopen}" "{\\isacharverbatimclose}" out, pos)] end
else if Token.is_kind Token.Cartouche tok then
- enclose "{\\isacartoucheopen}" "{\\isacartoucheclose}" (Latex.output_syms s)
- else Latex.output_syms s;
- in [Latex.text (output, Token.pos_of tok)] end
+ output_body state "{\\isacartoucheopen}" "{\\isacartoucheclose}" syms
+ else output_body state "" "" syms;
+ in output end
handle ERROR msg => error (msg ^ Position.here (Token.pos_of tok));
end;
+
+(** present theory source **)
+
+(*NB: arranging white space around command spans is a black art*)
+
+
(* presentation tokens *)
datatype token =
@@ -308,10 +337,8 @@
fun present_token state tok =
(case tok of
No_Token => []
- | Basic_Token tok => output_token tok
- | Markup_Token (cmd, source) =>
- Latex.string ("%\n\\isamarkup" ^ cmd ^ "{") ::
- output_text state {markdown = false} source @ [Latex.string "%\n}\n"]
+ | Basic_Token tok => output_token state tok
+ | Markup_Token (cmd, source) => output_markup state cmd source
| Markup_Env_Token (cmd, source) =>
[Latex.environment_block ("isamarkup" ^ cmd) (output_text state {markdown = true} source)]
| Raw_Token source =>