--- 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
--- 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
--- 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!
--- 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}}
--- 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"
--- 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)"
--- 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"
--- 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"
--- 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)"
--- 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;
--- 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 *)
--- 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 ||
--- 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
}
--- 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;
--- 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));