# HG changeset patch
# User wenzelm
# Date 1515838966 -3600
# Node ID 2555713586c8a8d1b39cd6f9c00b0ec9d2eec34c
# Parent  8b9d75d8f0b4341982f87b428df5a2452f464530
added \<^cancel> operator for unused text;

diff -r 8b9d75d8f0b4 -r 2555713586c8 NEWS
--- a/NEWS	Fri Jan 12 20:19:59 2018 +0100
+++ b/NEWS	Sat Jan 13 11:22:46 2018 +0100
@@ -118,6 +118,11 @@
 
 *** Document preparation ***
 
+* Unused formal text within inner syntax may be marked as
+\<^cancel>\<open>text\<close>. Thus it is ignored within the formal language, but
+still printed in the document (with special markup). This is an official
+way to "comment-out" some text.
+
 * Embedded languages such as inner syntax and ML may contain formal
 comments of the form "\<comment> \<open>text\<close>". As in marginal comments of outer
 syntax, antiquotations are interpreted wrt. the presentation context of
diff -r 8b9d75d8f0b4 -r 2555713586c8 etc/symbols
--- a/etc/symbols	Fri Jan 12 20:19:59 2018 +0100
+++ b/etc/symbols	Sat Jan 13 11:22:46 2018 +0100
@@ -388,6 +388,7 @@
 \<^action>              code: 0x00261b  group: icon  argument: cartouche  font: IsabelleText
 \<^assert>
 \<^binding>             argument: cartouche
+\<^cancel>              argument: cartouche
 \<^class>               argument: cartouche
 \<^class_syntax>        argument: cartouche
 \<^command_keyword>     argument: cartouche
diff -r 8b9d75d8f0b4 -r 2555713586c8 lib/texinputs/isabelle.sty
--- a/lib/texinputs/isabelle.sty	Fri Jan 12 20:19:59 2018 +0100
+++ b/lib/texinputs/isabelle.sty	Sat Jan 13 11:22:46 2018 +0100
@@ -41,6 +41,9 @@
 
 \newenvironment{isaantiq}{{\isacharat\isacharbraceleft}}{{\isacharbraceright}}
 
+\newcommand{\isamarkupcancel}[1]{\xout{#1}}  %requires \usepackage[normalem]{ulem}
+%OR: \newcommand{\isamarkupcancel}[1]{{\color{gray}{\isacharverbatimopen}#1{\isacharverbatimclose}}}  %requires \usepackage{xcolor}
+
 \newdimen\isa@parindent\newdimen\isa@parskip
 
 \newenvironment{isabellebody}{%
diff -r 8b9d75d8f0b4 -r 2555713586c8 lib/texinputs/isabellesym.sty
--- a/lib/texinputs/isabellesym.sty	Fri Jan 12 20:19:59 2018 +0100
+++ b/lib/texinputs/isabellesym.sty	Sat Jan 13 11:22:46 2018 +0100
@@ -368,6 +368,7 @@
 \newcommand{\isasymproof}{\isamath{\,\langle\mathit{proof}\rangle}}
 
 \newcommand{\isactrlassert}{\isakeywordcontrol{assert}}
+\newcommand{\isactrlcancel}{\isakeywordcontrol{cancel}}
 \newcommand{\isactrlbinding}{\isakeywordcontrol{binding}}
 \newcommand{\isactrlclass}{\isakeywordcontrol{class}}
 \newcommand{\isactrlclassUNDERSCOREsyntax}{\isakeywordcontrol{class{\isacharunderscore}syntax}}
diff -r 8b9d75d8f0b4 -r 2555713586c8 src/Pure/General/symbol.ML
--- a/src/Pure/General/symbol.ML	Fri Jan 12 20:19:59 2018 +0100
+++ b/src/Pure/General/symbol.ML	Sat Jan 13 11:22:46 2018 +0100
@@ -16,6 +16,7 @@
   val space: symbol
   val is_space: symbol -> bool
   val comment: symbol
+  val cancel: symbol
   val is_char: symbol -> bool
   val is_utf8: symbol -> bool
   val is_symbolic: symbol -> bool
@@ -107,6 +108,7 @@
 end;
 
 val comment = "\<comment>";
+val cancel = "\<^cancel>";
 
 fun is_char s = size s = 1;
 
diff -r 8b9d75d8f0b4 -r 2555713586c8 src/Pure/General/symbol_pos.ML
--- a/src/Pure/General/symbol_pos.ML	Fri Jan 12 20:19:59 2018 +0100
+++ b/src/Pure/General/symbol_pos.ML	Sat Jan 13 11:22:46 2018 +0100
@@ -34,6 +34,8 @@
   val scan_cartouche: string -> T list -> T list * T list
   val scan_cartouche_content: string -> T list -> T list * T list
   val recover_cartouche: T list -> T list * T list
+  val scan_blanks: T list -> T list * T list
+  val scan_cancel_cartouche: string -> T list -> T list * T list
   val scan_comment_cartouche: string -> T list -> T list * T list
   val scan_comment: string -> T list -> T list * T list
   val scan_comment_body: string -> T list -> T list * T list
@@ -216,10 +218,18 @@
 
 val recover_cartouche = Scan.pass (SOME 0) scan_cartouche_depth;
 
-fun scan_comment_cartouche err_prefix =
-  $$$ Symbol.comment @@@ Scan.many (Symbol.is_blank o symbol) @@@
-  !!! (fn () => err_prefix ^ "cartouche expected after " ^ quote Symbol.comment)
-    (scan_cartouche err_prefix);
+
+(* operator with cartouche argument *)
+
+val scan_blanks = Scan.many (Symbol.is_blank o symbol);
+
+fun scan_operator_cartouche blanks operator_symbol err_prefix =
+  (if blanks then $$$ operator_symbol @@@ scan_blanks else $$$ operator_symbol) @@@
+    !!! (fn () => err_prefix ^ "cartouche expected after " ^ quote operator_symbol)
+      (scan_cartouche err_prefix);
+
+val scan_cancel_cartouche = scan_operator_cartouche false Symbol.cancel;
+val scan_comment_cartouche = scan_operator_cartouche true Symbol.comment;
 
 
 (* ML-style comments *)
diff -r 8b9d75d8f0b4 -r 2555713586c8 src/Pure/Syntax/lexicon.ML
--- a/src/Pure/Syntax/lexicon.ML	Fri Jan 12 20:19:59 2018 +0100
+++ b/src/Pure/Syntax/lexicon.ML	Sat Jan 13 11:22:46 2018 +0100
@@ -22,7 +22,7 @@
   val is_tid: string -> bool
   datatype token_kind =
     Literal | IdentSy | LongIdentSy | VarSy | TFreeSy | TVarSy | NumSy | FloatSy |
-    StrSy | StringSy | Cartouche | Space | Comment | Comment_Cartouche | EOF
+    StrSy | StringSy | Cartouche | Space | Cancel | Comment | Comment_Cartouche | EOF
   datatype token = Token of token_kind * string * Position.range
   val kind_of_token: token -> token_kind
   val str_of_token: token -> string
@@ -114,7 +114,7 @@
 
 datatype token_kind =
   Literal | IdentSy | LongIdentSy | VarSy | TFreeSy | TVarSy | NumSy | FloatSy | StrSy |
-  StringSy | Cartouche | Space | Comment | Comment_Cartouche | EOF;
+  StringSy | Cartouche | Space | Cancel | Comment | Comment_Cartouche | EOF;
 
 datatype token = Token of token_kind * string * Position.range;
 
@@ -124,7 +124,7 @@
 
 val is_proper =
   kind_of_token #>
-  (fn Space => false | Comment => false | Comment_Cartouche => false | _ => true);
+  (fn Space => false | Cancel => false | Comment => false | Comment_Cartouche => false | _ => true);
 
 
 (* stopper *)
@@ -268,6 +268,7 @@
 
     val scan_token =
       Symbol_Pos.scan_cartouche err_prefix >> token Cartouche ||
+      Symbol_Pos.scan_cancel_cartouche Symbol.cancel >> token Cancel ||
       Symbol_Pos.scan_comment err_prefix >> token Comment ||
       Symbol_Pos.scan_comment_cartouche err_prefix >> token Comment_Cartouche ||
       Scan.max token_leq scan_lit scan_val ||
diff -r 8b9d75d8f0b4 -r 2555713586c8 src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Fri Jan 12 20:19:59 2018 +0100
+++ b/src/Pure/Thy/thy_output.ML	Sat Jan 13 11:22:46 2018 +0100
@@ -67,7 +67,34 @@
   end;
 
 
-(* output tokens with comments *)
+(* output tokens with operators *)
+
+datatype operator = No_Operator | Cancel | Comment;
+
+local
+
+open Basic_Symbol_Pos;
+
+fun is_operator sym = sym = Symbol.cancel orelse sym = Symbol.comment;
+
+fun scan_operator blanks operator_symbol operator =
+  (if blanks then $$$ operator_symbol @@@ Symbol_Pos.scan_blanks else $$$ operator_symbol) --
+    Scan.option (Symbol_Pos.scan_cartouche "Document token error: ")
+      >> (fn (syms, NONE) => (No_Operator, syms) | (_, SOME syms) => (operator, syms));
+
+val scan_symbols_operator =
+  Scan.many1 (fn (s, _) => not (is_operator s) andalso Symbol.not_eof s) >> pair No_Operator ||
+  scan_operator false Symbol.cancel Cancel ||
+  scan_operator true Symbol.comment Comment;
+
+in
+
+fun read_symbols_operator syms =
+  if exists (is_operator o Symbol_Pos.symbol) syms then
+    Scan.read Symbol_Pos.stopper (Scan.repeat scan_symbols_operator) syms
+  else NONE;
+
+end;
 
 local
 
@@ -82,31 +109,29 @@
     | Antiquote.Antiq {body, ...} =>
         Latex.enclose_body "%\n\\isaantiq\n" "{}%\n\\endisaantiq\n" (output_symbols body));
 
-fun output_symbols_comment ctxt {antiq} (is_comment, syms) =
-  if is_comment then
-    let
-      val content = Symbol_Pos.cartouche_content syms;
-      val source = Input.source true (Symbol_Pos.implode content) (Symbol_Pos.range content);
-    in Latex.enclose_body "%\n\\isamarkupcmt{" "}" (output_text ctxt {markdown = false} source) end
-  else if antiq then maps output_symbols_antiq (Antiquote.parse (#1 (Symbol_Pos.range syms)) 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 "Document token error: ")
-      >> (fn (syms, NONE) => (false, syms) | (_, SOME syms) => (true, syms));
-
-fun read_symbols_comment syms =
-  if exists (fn (s, _) => s = Symbol.comment) syms then
-    Scan.read Symbol_Pos.stopper (Scan.repeat scan_symbols_comment) syms
-  else NONE;
+fun output_symbols_operator ctxt {antiq} (operator, syms) =
+  (case (operator, antiq) of
+    (No_Operator, false) => output_symbols syms
+  | (No_Operator, true) =>
+      Antiquote.parse (#1 (Symbol_Pos.range syms)) syms
+      |> maps output_symbols_antiq
+  | (Cancel, _) =>
+      output_symbols (Symbol_Pos.cartouche_content syms)
+      |> Latex.enclose_body "%\n\\isamarkupcancel{" "}"
+  | (Comment, _) =>
+      let
+        val body = Symbol_Pos.cartouche_content syms;
+        val source = Input.source true (Symbol_Pos.implode body) (Symbol_Pos.range body);
+      in
+        output_text ctxt {markdown = false} source
+        |> Latex.enclose_body "%\n\\isamarkupcmt{" "}"
+      end);
 
 in
 
 fun output_body ctxt antiq bg en syms =
-  (case read_symbols_comment syms of
-    SOME res => maps (output_symbols_comment ctxt {antiq = antiq}) res
+  (case read_symbols_operator syms of
+    SOME res => maps (output_symbols_operator ctxt {antiq = antiq}) res
   | NONE => output_symbols syms) |> Latex.enclose_body bg en
 and output_token ctxt tok =
   let
@@ -128,17 +153,19 @@
   end handle ERROR msg => error (msg ^ Position.here (Token.pos_of tok));
 
 fun check_comments ctxt =
-  read_symbols_comment #> (Option.app o List.app) (fn (is_comment, syms) =>
+  read_symbols_operator #> (Option.app o List.app) (fn (operator, syms) =>
     let
       val pos = #1 (Symbol_Pos.range syms);
+      val markup =
+        (case operator of
+          No_Operator => NONE
+        | Cancel => SOME (Markup.language_text true)
+        | Comment => SOME (Markup.language_document true));
       val _ =
-        if is_comment then
-          Context_Position.reports ctxt
-            [(pos, Markup.language_document true),
-             (pos, Markup.cartouche)]
-        else ();
-      val _ = output_symbols_comment ctxt {antiq = false} (is_comment, syms);
-    in if is_comment then check_comments ctxt syms else () end);
+        markup |> Option.app (fn m =>
+          Context_Position.reports ctxt [(pos, m), (pos, Markup.cartouche)]);
+      val _ = output_symbols_operator ctxt {antiq = false} (operator, syms);
+    in if operator = Comment then check_comments ctxt syms else () end);
 
 fun check_token_comments ctxt tok =
   check_comments ctxt (Input.source_explode (Token.input_of tok));