--- a/src/Pure/General/comment.ML Sun Jan 14 15:31:02 2018 +0100
+++ b/src/Pure/General/comment.ML Sun Jan 14 16:21:29 2018 +0100
@@ -6,9 +6,11 @@
signature COMMENT =
sig
- datatype kind = Comment | Cancel
+ datatype kind = Comment | Cancel | Latex
+ val markup: kind -> Markup.T
val scan_comment: (kind * Symbol_Pos.T list) scanner
val scan_cancel: (kind * Symbol_Pos.T list) scanner
+ val scan_latex: (kind * Symbol_Pos.T list) scanner
val scan: (kind * Symbol_Pos.T list) scanner
val read_body: Symbol_Pos.T list -> (kind option * Symbol_Pos.T list) list option
end;
@@ -18,14 +20,16 @@
(* kinds *)
-datatype kind = Comment | Cancel;
+datatype kind = Comment | Cancel | Latex;
val kinds =
- [(Comment, {symbol = Symbol.comment, blanks = true}),
- (Cancel, {symbol = Symbol.cancel, blanks = false})];
+ [(Comment, {symbol = Symbol.comment, blanks = true, markup = Markup.language_document true}),
+ (Cancel, {symbol = Symbol.cancel, blanks = false, markup = Markup.language_text true}),
+ (Latex, {symbol = Symbol.latex, blanks = false, markup = Markup.language_latex true})];
val get_kind = the o AList.lookup (op =) kinds;
val print_kind = quote o #symbol o get_kind;
+val markup = #markup o get_kind;
fun is_symbol sym = exists (fn (_, {symbol, ...}) => symbol = sym) kinds;
@@ -41,7 +45,7 @@
val scan_blanks = Scan.many (Symbol.is_blank o Symbol_Pos.symbol);
fun scan_symbol kind =
- let val {blanks, symbol} = get_kind kind
+ let val {blanks, symbol, ...} = get_kind kind
in if blanks then $$$ symbol @@@ scan_blanks else $$$ symbol end;
fun scan_strict kind =
@@ -57,11 +61,12 @@
val scan_comment = scan_strict Comment;
val scan_cancel = scan_strict Cancel;
-val scan = scan_comment || scan_cancel;
+val scan_latex = scan_strict Latex;
+val scan = scan_comment || scan_cancel || scan_latex;
val scan_body =
Scan.many1 (fn (s, _) => not (is_symbol s) andalso Symbol.not_eof s) >> pair NONE ||
- scan_permissive Comment || scan_permissive Cancel;
+ scan_permissive Comment || scan_permissive Cancel || scan_permissive Latex;
fun read_body syms =
if exists (is_symbol o Symbol_Pos.symbol) syms then
--- a/src/Pure/PIDE/markup.ML Sun Jan 14 15:31:02 2018 +0100
+++ b/src/Pure/PIDE/markup.ML Sun Jan 14 16:21:29 2018 +0100
@@ -35,6 +35,7 @@
val language_antiquotation: T
val language_text: bool -> T
val language_verbatim: bool -> T
+ val language_latex: bool -> T
val language_rail: T
val language_path: T
val language_mixfix: T
@@ -296,6 +297,7 @@
language {name = "antiquotation", symbols = true, antiquotes = false, delimited = true};
val language_text = language' {name = "text", symbols = true, antiquotes = false};
val language_verbatim = language' {name = "verbatim_text", symbols = true, antiquotes = false};
+val language_latex = language' {name = "latex", symbols = false, antiquotes = false};
val language_rail = language {name = "rail", symbols = true, antiquotes = true, delimited = true};
val language_path = language {name = "path", symbols = false, antiquotes = false, delimited = true};
val language_mixfix =
--- a/src/Pure/Thy/thy_output.ML Sun Jan 14 15:31:02 2018 +0100
+++ b/src/Pure/Thy/thy_output.ML Sun Jan 14 16:21:29 2018 +0100
@@ -71,6 +71,9 @@
local
+fun output_latex syms =
+ [Latex.text (Symbol_Pos.content syms, #1 (Symbol_Pos.range syms))];
+
fun output_symbols syms =
[Latex.text (Latex.output_symbols (map Symbol_Pos.symbol syms), #1 (Symbol_Pos.range syms))];
@@ -98,7 +101,9 @@
end
| (SOME Comment.Cancel, _) =>
output_symbols (Symbol_Pos.cartouche_content syms)
- |> Latex.enclose_body "%\n\\isamarkupcancel{" "}");
+ |> Latex.enclose_body "%\n\\isamarkupcancel{" "}"
+ | (SOME Comment.Latex, _) =>
+ output_latex (Symbol_Pos.cartouche_content syms));
in
@@ -129,13 +134,9 @@
Comment.read_body #> (Option.app o List.app) (fn (comment, syms) =>
let
val pos = #1 (Symbol_Pos.range syms);
- val markup =
- comment |> Option.map
- (fn Comment.Comment => Markup.language_document true
- | Comment.Cancel => Markup.language_text true);
val _ =
- markup |> Option.app (fn m =>
- Context_Position.reports ctxt [(pos, m), (pos, Markup.cartouche)]);
+ comment |> Option.app (fn kind =>
+ Context_Position.reports ctxt [(pos, Comment.markup kind), (pos, Markup.cartouche)]);
val _ = output_symbols_comment ctxt {antiq = false} (comment, syms);
in if comment = SOME Comment.Comment then check_comments ctxt syms else () end);