# HG changeset patch
# User wenzelm
# Date 1515943289 -3600
# Node ID 95877cc6630e9e64bf56087438805d5a52bddb2e
# Parent  dd8e40f4696241821d4f8cdaf8d7c6c4a1ad5679
allow LaTeX source as formal comment;

diff -r dd8e40f46962 -r 95877cc6630e src/Pure/General/comment.ML
--- 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
diff -r dd8e40f46962 -r 95877cc6630e src/Pure/PIDE/markup.ML
--- 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 =
diff -r dd8e40f46962 -r 95877cc6630e src/Pure/Thy/thy_output.ML
--- 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);