# 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>\text\. 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 "\ \text\". 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 = "\"; +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));