# HG changeset patch
# User wenzelm
# Date 1515870139 -3600
# Node ID eec44c98d8b327b2a6870d0f0b1bec5f4b833854
# Parent  3f4b0c84630f2ad8fc864b2ad1687c04b4cdfe19# Parent  c4a10621c72e62f6aaed12b7bd1b5beacdbff66e
merged

diff -r 3f4b0c84630f -r eec44c98d8b3 NEWS
--- a/NEWS	Sat Jan 13 09:18:54 2018 +0000
+++ b/NEWS	Sat Jan 13 20:02:19 2018 +0100
@@ -118,6 +118,10 @@
 
 *** Document preparation ***
 
+* \<^cancel>\<open>text\<close> marks unused text within inner syntax: it is ignored
+within the formal language, but shown in the document with strike-out
+style.
+
 * 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 3f4b0c84630f -r eec44c98d8b3 etc/symbols
--- a/etc/symbols	Sat Jan 13 09:18:54 2018 +0000
+++ b/etc/symbols	Sat Jan 13 20:02:19 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 3f4b0c84630f -r eec44c98d8b3 lib/texinputs/isabelle.sty
--- a/lib/texinputs/isabelle.sty	Sat Jan 13 09:18:54 2018 +0000
+++ b/lib/texinputs/isabelle.sty	Sat Jan 13 20:02:19 2018 +0100
@@ -236,6 +236,12 @@
 }
 
 
+% cancel text
+
+\usepackage[normalem]{ulem}
+\newcommand{\isamarkupcancel}[1]{\xout{#1}}
+
+
 % tagged regions
 
 %plain TeX version of comment package -- much faster!
diff -r 3f4b0c84630f -r eec44c98d8b3 lib/texinputs/isabellesym.sty
--- a/lib/texinputs/isabellesym.sty	Sat Jan 13 09:18:54 2018 +0000
+++ b/lib/texinputs/isabellesym.sty	Sat Jan 13 20:02:19 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 3f4b0c84630f -r eec44c98d8b3 src/HOL/Nitpick_Examples/Hotel_Nits.thy
--- a/src/HOL/Nitpick_Examples/Hotel_Nits.thy	Sat Jan 13 09:18:54 2018 +0000
+++ b/src/HOL/Nitpick_Examples/Hotel_Nits.thy	Sat Jan 13 20:02:19 2018 +0100
@@ -44,7 +44,7 @@
 "\<lbrakk>s \<in> reach; (k,k') \<in> cards s g; roomk s r \<in> {k,k'}\<rbrakk> \<Longrightarrow>
  s\<lparr>isin := (isin s)(r := isin s r \<union> {g}),
    roomk := (roomk s)(r := k'),
-   safe := (safe s)(r := owns s r = Some g \<and> isin s r = {} \<comment> \<open>\<open>\<and> k' = currk s r\<close>\<close>
+   safe := (safe s)(r := owns s r = Some g \<and> isin s r = {} \<^cancel>\<open>\<and> k' = currk s r\<close>
                          \<or> safe s r)\<rparr> \<in> reach" |
 exit_room:
 "\<lbrakk>s \<in> reach; g \<in> isin s r\<rbrakk> \<Longrightarrow> s\<lparr>isin := (isin s)(r := isin s r - {g})\<rparr> \<in> reach"
diff -r 3f4b0c84630f -r eec44c98d8b3 src/HOL/Nitpick_Examples/Manual_Nits.thy
--- a/src/HOL/Nitpick_Examples/Manual_Nits.thy	Sat Jan 13 09:18:54 2018 +0000
+++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy	Sat Jan 13 20:02:19 2018 +0100
@@ -442,7 +442,7 @@
 primrec insort\<^sub>1 where
 "insort\<^sub>1 \<Lambda> x = N x 1 \<Lambda> \<Lambda>" |
 "insort\<^sub>1 (N y k t u) x =
- (* (split \<circ> skew) *) (N y k (if x < y then insort\<^sub>1 t x else t)
+ \<^cancel>\<open>(split \<circ> skew)\<close> (N y k (if x < y then insort\<^sub>1 t x else t)
                              (if x > y then insort\<^sub>1 u x else u))"
 
 theorem wf_insort\<^sub>1: "wf t \<Longrightarrow> wf (insort\<^sub>1 t x)"
diff -r 3f4b0c84630f -r eec44c98d8b3 src/HOL/Predicate_Compile_Examples/Hotel_Example.thy
--- a/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy	Sat Jan 13 09:18:54 2018 +0000
+++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy	Sat Jan 13 20:02:19 2018 +0100
@@ -52,7 +52,7 @@
   "roomk [] r = initk r"
 | "roomk (e#s) r = (let k = roomk s r in
     case e of Check_in g r' c \<Rightarrow> k
-            | Enter g r' (x,y) \<Rightarrow> if r' = r (*& x = k*) then y else k
+            | Enter g r' (x,y) \<Rightarrow> if r' = r \<^cancel>\<open>\<and> x = k\<close> then y else k
             | Exit g r \<Rightarrow> k)"
 
 primrec isin :: "event list \<Rightarrow> room \<Rightarrow> guest set"
diff -r 3f4b0c84630f -r eec44c98d8b3 src/HOL/Quickcheck_Examples/Hotel_Example.thy
--- a/src/HOL/Quickcheck_Examples/Hotel_Example.thy	Sat Jan 13 09:18:54 2018 +0000
+++ b/src/HOL/Quickcheck_Examples/Hotel_Example.thy	Sat Jan 13 20:02:19 2018 +0100
@@ -54,7 +54,7 @@
   "roomk [] r = initk r"
 | "roomk (e#s) r = (let k = roomk s r in
     case e of Check_in g r' c \<Rightarrow> k
-            | Enter g r' (x,y) \<Rightarrow> if r' = r (*& x = k*) then y else k
+            | Enter g r' (x,y) \<Rightarrow> if r' = r \<^cancel>\<open>\<and> x = k\<close> then y else k
             | Exit g r \<Rightarrow> k)"
 
 primrec isin :: "event list \<Rightarrow> room \<Rightarrow> guest set"
diff -r 3f4b0c84630f -r eec44c98d8b3 src/HOL/Quickcheck_Examples/Quickcheck_Narrowing_Examples.thy
--- a/src/HOL/Quickcheck_Examples/Quickcheck_Narrowing_Examples.thy	Sat Jan 13 09:18:54 2018 +0000
+++ b/src/HOL/Quickcheck_Examples/Quickcheck_Narrowing_Examples.thy	Sat Jan 13 20:02:19 2018 +0100
@@ -177,7 +177,7 @@
 fun l_bal where
 "l_bal(n, MKT ln ll lr h, r) =
  (if ht ll < ht lr
-  then case lr of ET \<Rightarrow> ET (* impossible *)
+  then case lr of ET \<Rightarrow> ET \<comment> \<open>impossible\<close>
                 | MKT lrn lrr lrl lrh \<Rightarrow>
                   mkt lrn (mkt ln ll lrl) (mkt n lrr r)
   else mkt ln ll (mkt n lr r))"
@@ -185,7 +185,7 @@
 fun r_bal where
 "r_bal(n, l, MKT rn rl rr h) =
  (if ht rl > ht rr
-  then case rl of ET \<Rightarrow> ET (* impossible *)
+  then case rl of ET \<Rightarrow> ET \<comment> \<open>impossible\<close>
                 | MKT rln rll rlr h \<Rightarrow> mkt rln (mkt n l rll) (mkt rn rlr rr)
   else mkt rn (mkt n l rl) rr)"
 
diff -r 3f4b0c84630f -r eec44c98d8b3 src/Pure/General/symbol.ML
--- a/src/Pure/General/symbol.ML	Sat Jan 13 09:18:54 2018 +0000
+++ b/src/Pure/General/symbol.ML	Sat Jan 13 20:02:19 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 3f4b0c84630f -r eec44c98d8b3 src/Pure/General/symbol_pos.ML
--- a/src/Pure/General/symbol_pos.ML	Sat Jan 13 09:18:54 2018 +0000
+++ b/src/Pure/General/symbol_pos.ML	Sat Jan 13 20:02:19 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 3f4b0c84630f -r eec44c98d8b3 src/Pure/Syntax/lexicon.ML
--- a/src/Pure/Syntax/lexicon.ML	Sat Jan 13 09:18:54 2018 +0000
+++ b/src/Pure/Syntax/lexicon.ML	Sat Jan 13 20:02:19 2018 +0100
@@ -22,8 +22,9 @@
   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
   val pos_of_token: token -> Position.T
   val is_proper: token -> bool
@@ -113,17 +114,17 @@
 
 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;
 
+fun kind_of_token (Token (k, _, _)) = k;
 fun str_of_token (Token (_, s, _)) = s;
 fun pos_of_token (Token (_, _, (pos, _))) = pos;
 
-fun is_proper (Token (Space, _, _)) = false
-  | is_proper (Token (Comment, _, _)) = false
-  | is_proper (Token (Comment_Cartouche, _, _)) = false
-  | is_proper _ = true;
+val is_proper =
+  kind_of_token #>
+  (fn Space => false | Cancel => false | Comment => false | Comment_Cartouche => false | _ => true);
 
 
 (* stopper *)
@@ -131,9 +132,7 @@
 fun mk_eof pos = Token (EOF, "", (pos, Position.none));
 val eof = mk_eof Position.none;
 
-fun is_eof (Token (EOF, _, _)) = true
-  | is_eof _ = false;
-
+fun is_eof tok = kind_of_token tok = EOF;
 val stopper = Scan.stopper (K eof) is_eof;
 
 
@@ -191,9 +190,8 @@
 
 (* valued_token *)
 
-fun valued_token (Token (Literal, _, _)) = false
-  | valued_token (Token (EOF, _, _)) = false
-  | valued_token _ = true;
+val valued_token =
+  kind_of_token #> (fn Literal => false | EOF => false | _ => true);
 
 
 (* predef_term *)
@@ -248,7 +246,7 @@
 
 (** tokenize **)
 
-fun token_leq (Token (_, s1, _), Token (_, s2, _)) = s1 <= s2;
+val token_leq = op <= o apply2 str_of_token;
 fun token kind ss = Token (kind, Symbol_Pos.content ss, Symbol_Pos.range ss);
 
 fun tokenize lex xids syms =
@@ -270,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 3f4b0c84630f -r eec44c98d8b3 src/Pure/Thy/latex.scala
--- a/src/Pure/Thy/latex.scala	Sat Jan 13 09:18:54 2018 +0000
+++ b/src/Pure/Thy/latex.scala	Sat Jan 13 20:02:19 2018 +0100
@@ -116,9 +116,9 @@
         }
     }
 
+    val Line_Error = """^l\.\d+ (.*)$""".r
     val More_Error =
       List(
-        """l\.\d+""",
         "<argument>",
         "<template>",
         "<recently read>",
@@ -136,18 +136,26 @@
         "<everyeof>",
         "<write>").mkString("^(?:", "|", ") (.*)$").r
 
+    def error_suffix1(lines: List[String]): Option[String] =
+    {
+      val lines1 = lines.take(20).takeWhile({ case File_Line_Error(_) => false case _ => true })
+      lines1.zipWithIndex.collectFirst({
+        case (Line_Error(msg), i) => cat_lines(lines1.take(i) ::: List(msg)) })
+    }
+    def error_suffix2(lines: List[String]): Option[String] =
+      lines match {
+        case More_Error(msg) :: _ => Some(msg)
+        case _ => None
+      }
+
     @tailrec def filter(lines: List[String], result: List[(String, Position.T)])
       : List[(String, Position.T)] =
     {
       lines match {
         case File_Line_Error((file, line, msg1)) :: rest1 =>
           val pos = tex_file_position(file, line)
-          rest1 match {
-            case More_Error(msg2) :: rest2 =>
-              filter(rest2, (Exn.cat_message(msg1, msg2), pos) :: result)
-            case _ =>
-              filter(rest1, (msg1, pos) :: result)
-          }
+          val msg2 = error_suffix1(rest1) orElse error_suffix2(rest1) getOrElse ""
+          filter(rest1, (Exn.cat_message(msg1, msg2), pos) :: result)
         case _ :: rest => filter(rest, result)
         case Nil => result.reverse
       }
diff -r 3f4b0c84630f -r eec44c98d8b3 src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Sat Jan 13 09:18:54 2018 +0000
+++ b/src/Pure/Thy/present.ML	Sat Jan 13 20:02:19 2018 +0100
@@ -191,7 +191,7 @@
   let
     val script =
       "isabelle document -d " ^ File.bash_path dir ^ " -o " ^ Bash.string format ^
-        " -n " ^ Bash.string name ^ " -t " ^ Bash.string tags;
+        " -n " ^ Bash.string name ^ (if tags = "" then "" else " -t " ^ Bash.string tags);
     val doc_path = Path.appends [dir, Path.parent, Path.basic name |> Path.ext format];
     val _ = if verbose then writeln script else ();
     val {out, err, rc, ...} = Bash.process script;
diff -r 3f4b0c84630f -r eec44c98d8b3 src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Sat Jan 13 09:18:54 2018 +0000
+++ b/src/Pure/Thy/thy_output.ML	Sat Jan 13 20:02:19 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{" "%\n}"
+      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));