--- 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
--- 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
--- 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}{%
--- 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}}
--- 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;
--- 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 *)
--- 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 ||
--- 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));