# HG changeset patch # User wenzelm # Date 1515359939 -3600 # Node ID 86aa6e2abee15f911ec164bce5f405cf26e9c86c # Parent 63d7aca15f6b1ae41f91bee3f9f75036dbfc0273# Parent 7360fe6bb423acd25202e38745d10aaa47e48db1 merged diff -r 63d7aca15f6b -r 86aa6e2abee1 NEWS --- a/NEWS Sun Jan 07 11:12:34 2018 +0100 +++ b/NEWS Sun Jan 07 22:18:59 2018 +0100 @@ -103,6 +103,11 @@ *** Document preparation *** +* 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 +the enclosing command. + * System option "document_tags" specifies a default for otherwise untagged commands. This is occasionally useful to control the global visibility of commands via session options (e.g. in ROOT). diff -r 63d7aca15f6b -r 86aa6e2abee1 src/Doc/Isar_Ref/Inner_Syntax.thy --- a/src/Doc/Isar_Ref/Inner_Syntax.thy Sun Jan 07 11:12:34 2018 +0100 +++ b/src/Doc/Isar_Ref/Inner_Syntax.thy Sun Jan 07 22:18:59 2018 +0100 @@ -565,6 +565,7 @@ @{syntax_def (inner) str_token} & = & \<^verbatim>\''\ \\\ \<^verbatim>\''\ \\ @{syntax_def (inner) string_token} & = & \<^verbatim>\"\ \\\ \<^verbatim>\"\ \\ @{syntax_def (inner) cartouche} & = & @{verbatim "\"} \\\ @{verbatim "\"} \\ + @{syntax_def (inner) comment_cartouche} & = & @{verbatim "\ \"} \\\ @{verbatim "\"} \\ \end{supertabular} \end{center} @@ -578,6 +579,11 @@ The derived categories @{syntax_def (inner) num_const}, and @{syntax_def (inner) float_const}, provide robust access to the respective tokens: the syntax tree holds a syntactic constant instead of a free variable. + + A @{syntax (inner) comment_cartouche} resembles the outer syntax notation + for marginal @{syntax_ref comment} (\secref{sec:comments}), but is + syntactically more restrictive: only the symbol-form with \<^verbatim>\\\ and text + cartouche is supported. \ diff -r 63d7aca15f6b -r 86aa6e2abee1 src/Doc/Isar_Ref/Synopsis.thy --- a/src/Doc/Isar_Ref/Synopsis.thy Sun Jan 07 11:12:34 2018 +0100 +++ b/src/Doc/Isar_Ref/Synopsis.thy Sun Jan 07 22:18:59 2018 +0100 @@ -952,10 +952,10 @@ notepad begin assume r: - "A\<^sub>1 \ A\<^sub>2 \ (* assumptions *) - (\x y. B\<^sub>1 x y \ C\<^sub>1 x y \ R) \ (* case 1 *) - (\x y. B\<^sub>2 x y \ C\<^sub>2 x y \ R) \ (* case 2 *) - R (* main conclusion *)" + "A\<^sub>1 \ A\<^sub>2 \ \ \assumptions\ + (\x y. B\<^sub>1 x y \ C\<^sub>1 x y \ R) \ \ \case 1\ + (\x y. B\<^sub>2 x y \ C\<^sub>2 x y \ R) \ \ \case 2\ + R \ \main conclusion\" have A\<^sub>1 and A\<^sub>2 \ then have R diff -r 63d7aca15f6b -r 86aa6e2abee1 src/HOL/Computational_Algebra/Polynomial.thy --- a/src/HOL/Computational_Algebra/Polynomial.thy Sun Jan 07 11:12:34 2018 +0100 +++ b/src/HOL/Computational_Algebra/Polynomial.thy Sun Jan 07 22:18:59 2018 +0100 @@ -2893,7 +2893,7 @@ where "divide_poly_main lc q r d dr (Suc n) = (let cr = coeff r dr; a = cr div lc; mon = monom a n in - if False \ a * lc = cr then (* False \ is only because of problem in function-package *) + if False \ a * lc = cr then \ \\False \\ is only because of problem in function-package\ divide_poly_main lc (q + mon) diff -r 63d7aca15f6b -r 86aa6e2abee1 src/HOL/Data_Structures/AA_Set.thy --- a/src/HOL/Data_Structures/AA_Set.thy Sun Jan 07 11:12:34 2018 +0100 +++ b/src/HOL/Data_Structures/AA_Set.thy Sun Jan 07 22:18:59 2018 +0100 @@ -29,7 +29,7 @@ fun split :: "'a aa_tree \ 'a aa_tree" where "split (Node lva t1 a (Node lvb t2 b (Node lvc t3 c t4))) = - (if lva = lvb \ lvb = lvc (* lva = lvc suffices *) + (if lva = lvb \ lvb = lvc \ \\lva = lvc\ suffices\ then Node (lva+1) (Node lva t1 a t2) b (Node lva t3 c t4) else Node lva t1 a (Node lvb t2 b (Node lvc t3 c t4)))" | "split t = t" diff -r 63d7aca15f6b -r 86aa6e2abee1 src/HOL/HOLCF/IOA/ABP/Spec.thy --- a/src/HOL/HOLCF/IOA/ABP/Spec.thy Sun Jan 07 11:12:34 2018 +0100 +++ b/src/HOL/HOLCF/IOA/ABP/Spec.thy Sun Jan 07 22:18:59 2018 +0100 @@ -22,7 +22,7 @@ in case fst(snd(tr)) of - Next => t=s | (* Note that there is condition as in Sender *) + Next => t=s | \ \Note that there is condition as in Sender\ S_msg(m) => t = s@[m] | R_msg(m) => s = (m#t) | S_pkt(pkt) => False | diff -r 63d7aca15f6b -r 86aa6e2abee1 src/HOL/Nitpick_Examples/Hotel_Nits.thy --- a/src/HOL/Nitpick_Examples/Hotel_Nits.thy Sun Jan 07 11:12:34 2018 +0100 +++ b/src/HOL/Nitpick_Examples/Hotel_Nits.thy Sun Jan 07 22:18:59 2018 +0100 @@ -44,7 +44,7 @@ "\s \ reach; (k,k') \ cards s g; roomk s r \ {k,k'}\ \ s\isin := (isin s)(r := isin s r \ {g}), roomk := (roomk s)(r := k'), - safe := (safe s)(r := owns s r = Some g \ isin s r = {} (* \ k' = currk s r *) + safe := (safe s)(r := owns s r = Some g \ isin s r = {} \ \\\ k' = currk s r\\ \ safe s r)\ \ reach" | exit_room: "\s \ reach; g \ isin s r\ \ s\isin := (isin s)(r := isin s r - {g})\ \ reach" diff -r 63d7aca15f6b -r 86aa6e2abee1 src/HOL/Quickcheck_Exhaustive.thy --- a/src/HOL/Quickcheck_Exhaustive.thy Sun Jan 07 11:12:34 2018 +0100 +++ b/src/HOL/Quickcheck_Exhaustive.thy Sun Jan 07 22:18:59 2018 +0100 @@ -725,7 +725,7 @@ Some x \ Some x | None \ full_exhaustive_class.full_exhaustive (\(num, t). f (char_of_nat (nat_of_num num), \_ :: unit. Code_Evaluation.App (Code_Evaluation.Const (STR ''String.Char'') TYPEREP(num \ char)) (t ()))) - (min (i - 1) 8) (* generate at most 8 bits *) + (min (i - 1) 8) \ \generate at most 8 bits\ else None)" instance .. diff -r 63d7aca15f6b -r 86aa6e2abee1 src/Pure/General/scan.scala --- a/src/Pure/General/scan.scala Sun Jan 07 11:12:34 2018 +0100 +++ b/src/Pure/General/scan.scala Sun Jan 07 22:18:59 2018 +0100 @@ -27,6 +27,8 @@ case class Quoted(quote: String) extends Line_Context case object Verbatim extends Line_Context case class Cartouche(depth: Int) extends Line_Context + case object Comment_Prefix extends Line_Context + case class Cartouche_Comment(depth: Int) extends Line_Context case class Comment(depth: Int) extends Line_Context @@ -203,17 +205,16 @@ def cartouche_line(ctxt: Line_Context): Parser[(String, Line_Context)] = { - val depth = - ctxt match { - case Finished => 0 - case Cartouche(d) => d - case _ => -1 - } - if (depth >= 0) - cartouche_depth(depth) ^^ - { case (x, 0) => (x, Finished) - case (x, d) => (x, Cartouche(d)) } - else failure("") + def cartouche_context(d: Int): Line_Context = + if (d == 0) Finished else Cartouche(d) + + ctxt match { + case Finished => + cartouche_depth(0) ^^ { case (c, d) => (c, cartouche_context(d)) } + case Cartouche(depth) => + cartouche_depth(depth) ^^ { case (c, d) => (c, cartouche_context(d)) } + case _ => failure("") + } } val recover_cartouche: Parser[String] = @@ -229,6 +230,34 @@ Library.try_unsuffix(Symbol.close, source1) getOrElse err() } + def comment_prefix: Parser[String] = + (Symbol.comment | Symbol.comment_decoded) ~ many(Symbol.is_blank) ^^ + { case a ~ b => a + b.mkString } + + def comment_cartouche: Parser[String] = + comment_prefix ~ cartouche ^^ { case a ~ b => a + b } + + def comment_cartouche_line(ctxt: Line_Context): Parser[(String, Line_Context)] = + { + def cartouche_context(d: Int): Line_Context = + if (d == 0) Finished else Cartouche_Comment(d) + + ctxt match { + case Finished => + comment_prefix ~ opt(cartouche_depth(0)) ^^ { + case a ~ None => (a, Comment_Prefix) + case a ~ Some((c, d)) => (a + c, cartouche_context(d)) } + case Comment_Prefix => + many1(Symbol.is_blank) ~ opt(cartouche_depth(0)) ^^ { + case b ~ None => (b.mkString, Comment_Prefix) + case b ~ Some((c, d)) => (b.mkString + c, cartouche_context(d)) } | + cartouche_depth(0) ^^ { case (c, d) => (c, cartouche_context(d)) } + case Cartouche_Comment(depth) => + cartouche_depth(depth) ^^ { case (c, d) => (c, cartouche_context(d)) } + case _ => failure("") + } + } + /* nested comments */ diff -r 63d7aca15f6b -r 86aa6e2abee1 src/Pure/General/symbol_pos.ML --- a/src/Pure/General/symbol_pos.ML Sun Jan 07 11:12:34 2018 +0100 +++ b/src/Pure/General/symbol_pos.ML Sun Jan 07 22:18:59 2018 +0100 @@ -34,6 +34,7 @@ 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_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 val recover_comment: T list -> T list * T list @@ -215,6 +216,11 @@ 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); + (* ML-style comments *) diff -r 63d7aca15f6b -r 86aa6e2abee1 src/Pure/ML/ml_compiler.ML --- a/src/Pure/ML/ml_compiler.ML Sun Jan 07 11:12:34 2018 +0100 +++ b/src/Pure/ML/ml_compiler.ML Sun Jan 07 22:18:59 2018 +0100 @@ -173,8 +173,12 @@ if #SML flags then String.explode else maps (String.explode o Symbol.esc) o Symbol.explode; + fun token_content tok = + if ML_Lex.is_comment tok then NONE + else SOME (input_explode (ML_Lex.check_content_of tok), tok); + val input_buffer = - Unsynchronized.ref (toks |> map (`(input_explode o ML_Lex.check_content_of))); + Unsynchronized.ref (map_filter token_content toks); fun get () = (case ! input_buffer of diff -r 63d7aca15f6b -r 86aa6e2abee1 src/Pure/ML/ml_lex.ML --- a/src/Pure/ML/ml_lex.ML Sun Jan 07 11:12:34 2018 +0100 +++ b/src/Pure/ML/ml_lex.ML Sun Jan 07 22:18:59 2018 +0100 @@ -9,11 +9,12 @@ val keywords: string list datatype token_kind = Keyword | Ident | Long_Ident | Type_Var | Word | Int | Real | Char | String | - Space | Comment | Error of string | EOF + Space | Comment | Comment_Cartouche | Error of string | EOF eqtype token val stopper: token Scan.stopper val is_regular: token -> bool val is_improper: token -> bool + val is_comment: token -> bool val set_range: Position.range -> token -> token val range_of: token -> Position.range val pos_of: token -> Position.T @@ -63,7 +64,7 @@ datatype token_kind = Keyword | Ident | Long_Ident | Type_Var | Word | Int | Real | Char | String | - Space | Comment | Error of string | EOF; + Space | Comment | Comment_Cartouche | Error of string | EOF; datatype token = Token of Position.range * (token_kind * string); @@ -108,8 +109,13 @@ fun is_improper (Token (_, (Space, _))) = true | is_improper (Token (_, (Comment, _))) = true + | is_improper (Token (_, (Comment_Cartouche, _))) = true | is_improper _ = false; +fun is_comment (Token (_, (Comment, _))) = true + | is_comment (Token (_, (Comment_Cartouche, _))) = true + | is_comment _ = false; + fun warn tok = (case tok of Token (_, (Keyword, ":>")) => @@ -147,6 +153,7 @@ | Char => (Markup.ML_char, "") | String => (if SML then Markup.SML_string else Markup.ML_string, "") | Comment => (if SML then Markup.SML_comment else Markup.ML_comment, "") + | Comment_Cartouche => (if SML then Markup.SML_comment else Markup.ML_comment, "") | Error msg => (Markup.bad (), msg) | _ => (Markup.empty, ""); @@ -171,6 +178,7 @@ open Basic_Symbol_Pos; val err_prefix = "SML lexical error: "; +val err_prefix' = "Isabelle/ML lexical error: "; fun !!! msg = Symbol_Pos.!!! (fn () => err_prefix ^ msg); @@ -292,6 +300,7 @@ scan_string >> token String || scan_blanks1 >> token Space || Symbol_Pos.scan_comment err_prefix >> token Comment || + Symbol_Pos.scan_comment_cartouche err_prefix' >> token Comment_Cartouche || Scan.max token_leq (Scan.literal lexicon >> token Keyword) (scan_word >> token Word || diff -r 63d7aca15f6b -r 86aa6e2abee1 src/Pure/ML/ml_lex.scala --- a/src/Pure/ML/ml_lex.scala Sun Jan 07 11:12:34 2018 +0100 +++ b/src/Pure/ML/ml_lex.scala Sun Jan 07 22:18:59 2018 +0100 @@ -51,6 +51,7 @@ val STRING = Value("quoted string") val SPACE = Value("white space") val COMMENT = Value("comment text") + val COMMENT_CARTOUCHE = Value("comment cartouche") val CONTROL = Value("control symbol antiquotation") val ANTIQ = Value("antiquotation") val ANTIQ_START = Value("antiquotation: start") @@ -67,7 +68,7 @@ def is_keyword: Boolean = kind == Kind.KEYWORD def is_delimiter: Boolean = is_keyword && !Symbol.is_ascii_identifier(source) def is_space: Boolean = kind == Kind.SPACE - def is_comment: Boolean = kind == Kind.COMMENT + def is_comment: Boolean = kind == Kind.COMMENT || kind == Kind.COMMENT_CARTOUCHE } @@ -144,17 +145,45 @@ private def ml_comment_line(ctxt: Scan.Line_Context): Parser[(Token, Scan.Line_Context)] = comment_line(ctxt) ^^ { case (x, c) => (Token(Kind.COMMENT, x), c) } + private val ml_comment_cartouche: Parser[Token] = + comment_cartouche ^^ (x => Token(Kind.COMMENT_CARTOUCHE, x)) - /* delimited token */ + private def ml_comment_cartouche_line(ctxt: Scan.Line_Context) + : Parser[(Token, Scan.Line_Context)] = + comment_cartouche_line(ctxt) ^^ { case (x, c) => (Token(Kind.COMMENT_CARTOUCHE, x), c) } + + + /* antiquotations (line-oriented) */ + + def ml_cartouche_line(ctxt: Scan.Line_Context): Parser[(Token, Scan.Line_Context)] = + cartouche_line(ctxt) ^^ { case (x, c) => (Token(Kind.ANTIQ_CARTOUCHE, x), c) } + + def ml_antiq_start(ctxt: Scan.Line_Context): Parser[(Token, Scan.Line_Context)] = + ctxt match { + case Scan.Finished => "@{" ^^ (x => (Token(Kind.ANTIQ_START, x), Antiq(Scan.Finished))) + case _ => failure("") + } - private def delimited_token: Parser[Token] = - ml_char | (ml_string | ml_comment) + def ml_antiq_stop(ctxt: Scan.Line_Context): Parser[(Token, Scan.Line_Context)] = + ctxt match { + case Antiq(Scan.Finished) => "}" ^^ (x => (Token(Kind.ANTIQ_STOP, x), Scan.Finished)) + case _ => failure("") + } - private val recover_delimited: Parser[Token] = - (recover_ml_char | (recover_ml_string | (recover_cartouche | recover_comment))) ^^ - (x => Token(Kind.ERROR, x)) + def ml_antiq_body(context: Scan.Line_Context): Parser[(Token, Scan.Line_Context)] = + context match { + case Antiq(ctxt) => + (if (ctxt == Scan.Finished) antiq_other ^^ (x => (Token(Kind.ANTIQ_OTHER, x), context)) + else failure("")) | + quoted_line("\"", ctxt) ^^ { case (x, c) => (Token(Kind.ANTIQ_STRING, x), Antiq(c)) } | + quoted_line("`", ctxt) ^^ { case (x, c) => (Token(Kind.ANTIQ_ALT_STRING, x), Antiq(c)) } | + cartouche_line(ctxt) ^^ { case (x, c) => (Token(Kind.ANTIQ_CARTOUCHE, x), Antiq(c)) } + case _ => failure("") + } + /* token */ + private def other_token: Parser[Token] = { /* identifiers */ @@ -214,54 +243,29 @@ val bad = one(_ => true) ^^ (x => Token(Kind.ERROR, x)) - space | (ml_control | (recover_delimited | (ml_antiq | + val recover = + (recover_ml_char | (recover_ml_string | (recover_cartouche | recover_comment))) ^^ + (x => Token(Kind.ERROR, x)) + + space | (ml_control | (recover | (ml_antiq | (((word | (real | (int | (long_ident | (ident | type_var))))) ||| keyword) | bad)))) } - - /* antiquotations (line-oriented) */ - - def ml_cartouche_line(ctxt: Scan.Line_Context): Parser[(Token, Scan.Line_Context)] = - cartouche_line(ctxt) ^^ { case (x, c) => (Token(Kind.ANTIQ_CARTOUCHE, x), c) } - - def ml_antiq_start(ctxt: Scan.Line_Context): Parser[(Token, Scan.Line_Context)] = - ctxt match { - case Scan.Finished => "@{" ^^ (x => (Token(Kind.ANTIQ_START, x), Antiq(Scan.Finished))) - case _ => failure("") - } - - def ml_antiq_stop(ctxt: Scan.Line_Context): Parser[(Token, Scan.Line_Context)] = - ctxt match { - case Antiq(Scan.Finished) => "}" ^^ (x => (Token(Kind.ANTIQ_STOP, x), Scan.Finished)) - case _ => failure("") - } - - def ml_antiq_body(context: Scan.Line_Context): Parser[(Token, Scan.Line_Context)] = - context match { - case Antiq(ctxt) => - (if (ctxt == Scan.Finished) antiq_other ^^ (x => (Token(Kind.ANTIQ_OTHER, x), context)) - else failure("")) | - quoted_line("\"", ctxt) ^^ { case (x, c) => (Token(Kind.ANTIQ_STRING, x), Antiq(c)) } | - quoted_line("`", ctxt) ^^ { case (x, c) => (Token(Kind.ANTIQ_ALT_STRING, x), Antiq(c)) } | - cartouche_line(ctxt) ^^ { case (x, c) => (Token(Kind.ANTIQ_CARTOUCHE, x), Antiq(c)) } - case _ => failure("") - } - - - /* token */ - - def token: Parser[Token] = delimited_token | other_token + def token: Parser[Token] = + ml_char | (ml_string | (ml_comment | (ml_comment_cartouche | other_token))) def token_line(SML: Boolean, ctxt: Scan.Line_Context): Parser[(Token, Scan.Line_Context)] = { val other = (ml_char | other_token) ^^ (x => (x, Scan.Finished)) if (SML) ml_string_line(ctxt) | (ml_comment_line(ctxt) | other) - else + else { ml_string_line(ctxt) | (ml_comment_line(ctxt) | - (ml_cartouche_line(ctxt) | - (ml_antiq_start(ctxt) | (ml_antiq_stop(ctxt) | (ml_antiq_body(ctxt) | other))))) + (ml_comment_cartouche_line(ctxt) | + (ml_cartouche_line(ctxt) | + (ml_antiq_start(ctxt) | (ml_antiq_stop(ctxt) | (ml_antiq_body(ctxt) | other)))))) + } } } diff -r 63d7aca15f6b -r 86aa6e2abee1 src/Pure/Syntax/lexicon.ML --- a/src/Pure/Syntax/lexicon.ML Sun Jan 07 11:12:34 2018 +0100 +++ b/src/Pure/Syntax/lexicon.ML Sun Jan 07 22:18:59 2018 +0100 @@ -21,8 +21,8 @@ val scan_tvar: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list val is_tid: string -> bool datatype token_kind = - Literal | IdentSy | LongIdentSy | VarSy | TFreeSy | TVarSy | NumSy | - FloatSy | StrSy | StringSy | Cartouche | Space | Comment | EOF + Literal | IdentSy | LongIdentSy | VarSy | TFreeSy | TVarSy | NumSy | FloatSy | + StrSy | StringSy | Cartouche | Space | Comment | Comment_Cartouche | EOF datatype token = Token of token_kind * string * Position.range val str_of_token: token -> string val pos_of_token: token -> Position.T @@ -112,8 +112,8 @@ (** datatype token **) datatype token_kind = - Literal | IdentSy | LongIdentSy | VarSy | TFreeSy | TVarSy | NumSy | - FloatSy | StrSy | StringSy | Cartouche | Space | Comment | EOF; + Literal | IdentSy | LongIdentSy | VarSy | TFreeSy | TVarSy | NumSy | FloatSy | StrSy | + StringSy | Cartouche | Space | Comment | Comment_Cartouche | EOF; datatype token = Token of token_kind * string * Position.range; @@ -122,6 +122,7 @@ fun is_proper (Token (Space, _, _)) = false | is_proper (Token (Comment, _, _)) = false + | is_proper (Token (Comment_Cartouche, _, _)) = false | is_proper _ = true; @@ -170,6 +171,7 @@ | StringSy => Markup.inner_string | Cartouche => Markup.inner_cartouche | Comment => Markup.inner_comment + | Comment_Cartouche => Markup.inner_comment | _ => Markup.empty; fun report_of_token (Token (kind, s, (pos, _))) = @@ -270,6 +272,7 @@ val scan_token = Symbol_Pos.scan_cartouche err_prefix >> token Cartouche || 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 || scan_string >> token StringSy || scan_str >> token StrSy || diff -r 63d7aca15f6b -r 86aa6e2abee1 src/Pure/Thy/document_antiquotations.ML --- a/src/Pure/Thy/document_antiquotations.ML Sun Jan 07 11:12:34 2018 +0100 +++ b/src/Pure/Thy/document_antiquotations.ML Sun Jan 07 22:18:59 2018 +0100 @@ -84,7 +84,7 @@ val _ = Theory.setup (Thy_Output.antiquotation \<^binding>\theory_text\ (Scan.lift Args.text_input) - (fn {context = ctxt, ...} => fn source => + (fn {state, context = ctxt, ...} => fn source => let val _ = Context_Position.report ctxt (Input.pos_of source) @@ -101,7 +101,7 @@ val indentation = Latex.output_symbols (replicate (Config.get ctxt Thy_Output.indent) Symbol.space); in - implode (map Latex.output_token toks) |> + Latex.output_text (maps (Thy_Output.output_token state) toks) |> (if Config.get ctxt Thy_Output.display then split_lines #> map (prefix indentation) #> cat_lines #> Latex.environment "isabelle" diff -r 63d7aca15f6b -r 86aa6e2abee1 src/Pure/Thy/latex.ML --- a/src/Pure/Thy/latex.ML Sun Jan 07 11:12:34 2018 +0100 +++ b/src/Pure/Thy/latex.ML Sun Jan 07 22:18:59 2018 +0100 @@ -20,7 +20,6 @@ val embed_raw: string -> string val output_symbols: Symbol.symbol list -> string val output_syms: string -> string - val output_token: Token.T -> string val begin_delim: string -> string val end_delim: string -> string val begin_tag: string -> string @@ -76,7 +75,9 @@ end; -fun enclose_body bg en body = string bg :: body @ [string en]; +fun enclose_body bg en body = + (if bg = "" then [] else [string bg]) @ body @ + (if en = "" then [] else [string en]); (* output name for LaTeX macros *) @@ -202,45 +203,9 @@ val output_syms = output_symbols o Symbol.explode; -val output_syms_antiq = - (fn Antiquote.Text ss => output_symbols (map Symbol_Pos.symbol ss) - | Antiquote.Control {name = (name, _), body, ...} => - "\\isaantiqcontrol{" ^ output_symbols (Symbol.explode name) ^ "}" ^ - output_symbols (map Symbol_Pos.symbol body) - | Antiquote.Antiq {body, ...} => - enclose "%\n\\isaantiq\n" "{}%\n\\endisaantiq\n" - (output_symbols (map Symbol_Pos.symbol body))); - end; -(* output token *) - -fun output_token tok = - let - val s = Token.content_of tok; - val output = - if Token.is_kind Token.Comment tok then "" - else if Token.is_command tok then - "\\isacommand{" ^ output_syms s ^ "}" - else if Token.is_kind Token.Keyword tok andalso Symbol.is_ascii_identifier s then - "\\isakeyword{" ^ output_syms s ^ "}" - else if Token.is_kind Token.String tok then - enclose "{\\isachardoublequoteopen}" "{\\isachardoublequoteclose}" (output_syms s) - else if Token.is_kind Token.Alt_String tok then - enclose "{\\isacharbackquoteopen}" "{\\isacharbackquoteclose}" (output_syms s) - else if Token.is_kind Token.Verbatim tok then - let - val ants = Antiquote.read (Token.input_of tok); - val out = implode (map output_syms_antiq ants); - in enclose "{\\isacharverbatimopen}" "{\\isacharverbatimclose}" out end - else if Token.is_kind Token.Cartouche tok then - enclose "{\\isacartoucheopen}" "{\\isacartoucheclose}" (output_syms s) - else output_syms s; - in output end - handle ERROR msg => error (msg ^ Position.here (Token.pos_of tok)); - - (* tags *) val begin_delim = enclose_name "%\n\\isadelim" "\n"; diff -r 63d7aca15f6b -r 86aa6e2abee1 src/Pure/Thy/thy_output.ML --- a/src/Pure/Thy/thy_output.ML Sun Jan 07 11:12:34 2018 +0100 +++ b/src/Pure/Thy/thy_output.ML Sun Jan 07 22:18:59 2018 +0100 @@ -25,6 +25,7 @@ val integer: string -> int val eval_antiquote: Toplevel.state -> Antiquote.text_antiquote -> string val output_text: Toplevel.state -> {markdown: bool} -> Input.source -> Latex.text list + val output_token: Toplevel.state -> Token.T -> Latex.text list val present_thy: theory -> (Toplevel.transition * Toplevel.state) list -> Token.T list -> Latex.text list val pretty_text: Proof.context -> string -> Pretty.T @@ -192,6 +193,9 @@ end; + +(** document output **) + (* output text *) fun output_text state {markdown} source = @@ -240,15 +244,77 @@ end; +(* output tokens with comments *) + +local + +fun output_symbols syms = + [Latex.text (Latex.output_symbols (map Symbol_Pos.symbol syms), #1 (Symbol_Pos.range syms))]; + +val output_symbols_antiq = + (fn Antiquote.Text syms => output_symbols syms + | Antiquote.Control {name = (name, _), body, ...} => + Latex.string ("\\isaantiqcontrol{" ^ Latex.output_symbols (Symbol.explode name) ^ "}") :: + output_symbols body + | Antiquote.Antiq {body, ...} => + Latex.enclose_body "%\n\\isaantiq\n" "{}%\n\\endisaantiq\n" (output_symbols body)); + +fun output_symbols_comment state {antiq} (is_comment, syms) = + if is_comment then + Latex.enclose_body ("%\n\\isamarkupcmt{") "}" + (output_text state {markdown = false} + (Input.source true (Symbol_Pos.implode syms) (Symbol_Pos.range syms))) + 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_content "Document token error: ") + >> (fn (syms, NONE) => (false, syms) | (_, SOME syms) => (true, syms)); + +in + +fun output_body state antiq bg en syms = + (if exists (fn (s, _) => s = Symbol.comment) syms then + (case Scan.read Symbol_Pos.stopper (Scan.repeat scan_symbols_comment) syms of + SOME res => maps (output_symbols_comment state {antiq = antiq}) res + | NONE => output_symbols syms) + else output_symbols syms) |> Latex.enclose_body bg en +and output_token state tok = + let + val syms = Input.source_explode (Token.input_of tok); + val output = + if Token.is_kind Token.Comment tok then [] + else if Token.is_command tok then output_body state false "\\isacommand{" "}" syms + else if Token.is_kind Token.Keyword tok andalso + Symbol.is_ascii_identifier (Token.content_of tok) + then output_body state false "\\isakeyword{" "}" syms + else if Token.is_kind Token.String tok then + output_body state false "{\\isachardoublequoteopen}" "{\\isachardoublequoteclose}" syms + else if Token.is_kind Token.Alt_String tok then + output_body state false "{\\isacharbackquoteopen}" "{\\isacharbackquoteclose}" syms + else if Token.is_kind Token.Verbatim tok then + output_body state true "{\\isacharverbatimopen}" "{\\isacharverbatimclose}" syms + else if Token.is_kind Token.Cartouche tok then + output_body state false "{\\isacartoucheopen}" "{\\isacartoucheclose}" syms + else output_body state false "" "" syms; + in output end + handle ERROR msg => error (msg ^ Position.here (Token.pos_of tok)); + +end; + + (** present theory source **) (*NB: arranging white space around command spans is a black art*) + (* presentation tokens *) datatype token = - No_Token + Ignore_Token | Basic_Token of Token.T | Markup_Token of string * Input.source | Markup_Env_Token of string * Input.source @@ -264,11 +330,11 @@ fun present_token state tok = (case tok of - No_Token => [] - | Basic_Token tok => [Latex.text (Latex.output_token tok, Token.pos_of tok)] + Ignore_Token => [] + | Basic_Token tok => output_token state tok | Markup_Token (cmd, source) => - Latex.string ("%\n\\isamarkup" ^ cmd ^ "{") :: - output_text state {markdown = false} source @ [Latex.string "%\n}\n"] + Latex.enclose_body ("%\n\\isamarkup" ^ cmd ^ "{") "%\n}\n" + (output_text state {markdown = false} source) | Markup_Env_Token (cmd, source) => [Latex.environment_block ("isamarkup" ^ cmd) (output_text state {markdown = true} source)] | Raw_Token source => @@ -418,7 +484,7 @@ (* tokens *) val ignored = Scan.state --| ignore - >> (fn d => (NONE, (No_Token, ("", d)))); + >> (fn d => (NONE, (Ignore_Token, ("", d)))); fun markup pred mk flag = Scan.peek (fn d => improper |-- diff -r 63d7aca15f6b -r 86aa6e2abee1 src/Tools/jEdit/src/jedit_rendering.scala --- a/src/Tools/jEdit/src/jedit_rendering.scala Sun Jan 07 11:12:34 2018 +0100 +++ b/src/Tools/jEdit/src/jedit_rendering.scala Sun Jan 07 22:18:59 2018 +0100 @@ -89,6 +89,7 @@ ML_Lex.Kind.STRING -> LITERAL1, ML_Lex.Kind.SPACE -> NULL, ML_Lex.Kind.COMMENT -> COMMENT1, + ML_Lex.Kind.COMMENT_CARTOUCHE -> COMMENT1, ML_Lex.Kind.ANTIQ -> NULL, ML_Lex.Kind.ANTIQ_START -> LITERAL4, ML_Lex.Kind.ANTIQ_STOP -> LITERAL4,