--- 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 "\<comment> \<open>text\<close>". 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).
--- 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>\<open>''\<close> \<open>\<dots>\<close> \<^verbatim>\<open>''\<close> \\
@{syntax_def (inner) string_token} & = & \<^verbatim>\<open>"\<close> \<open>\<dots>\<close> \<^verbatim>\<open>"\<close> \\
@{syntax_def (inner) cartouche} & = & @{verbatim "\<open>"} \<open>\<dots>\<close> @{verbatim "\<close>"} \\
+ @{syntax_def (inner) comment_cartouche} & = & @{verbatim "\<comment> \<open>"} \<open>\<dots>\<close> @{verbatim "\<close>"} \\
\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>\<open>\<comment>\<close> and text
+ cartouche is supported.
\<close>
--- 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 \<Longrightarrow> A\<^sub>2 \<Longrightarrow> (* assumptions *)
- (\<And>x y. B\<^sub>1 x y \<Longrightarrow> C\<^sub>1 x y \<Longrightarrow> R) \<Longrightarrow> (* case 1 *)
- (\<And>x y. B\<^sub>2 x y \<Longrightarrow> C\<^sub>2 x y \<Longrightarrow> R) \<Longrightarrow> (* case 2 *)
- R (* main conclusion *)"
+ "A\<^sub>1 \<Longrightarrow> A\<^sub>2 \<Longrightarrow> \<comment> \<open>assumptions\<close>
+ (\<And>x y. B\<^sub>1 x y \<Longrightarrow> C\<^sub>1 x y \<Longrightarrow> R) \<Longrightarrow> \<comment> \<open>case 1\<close>
+ (\<And>x y. B\<^sub>2 x y \<Longrightarrow> C\<^sub>2 x y \<Longrightarrow> R) \<Longrightarrow> \<comment> \<open>case 2\<close>
+ R \<comment> \<open>main conclusion\<close>"
have A\<^sub>1 and A\<^sub>2 \<proof>
then have R
--- 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 \<or> a * lc = cr then (* False \<or> is only because of problem in function-package *)
+ if False \<or> a * lc = cr then \<comment> \<open>\<open>False \<or>\<close> is only because of problem in function-package\<close>
divide_poly_main
lc
(q + mon)
--- 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 \<Rightarrow> 'a aa_tree" where
"split (Node lva t1 a (Node lvb t2 b (Node lvc t3 c t4))) =
- (if lva = lvb \<and> lvb = lvc (* lva = lvc suffices *)
+ (if lva = lvb \<and> lvb = lvc \<comment> \<open>\<open>lva = lvc\<close> suffices\<close>
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"
--- 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 | \<comment> \<open>Note that there is condition as in Sender\<close>
S_msg(m) => t = s@[m] |
R_msg(m) => s = (m#t) |
S_pkt(pkt) => False |
--- 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 @@
"\<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 = {} (* \<and> k' = currk s r *)
+ safe := (safe s)(r := owns s r = Some g \<and> isin s r = {} \<comment> \<open>\<open>\<and> k' = currk s r\<close>\<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/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 \<Rightarrow> Some x
| None \<Rightarrow> full_exhaustive_class.full_exhaustive
(\<lambda>(num, t). f (char_of_nat (nat_of_num num), \<lambda>_ :: unit. Code_Evaluation.App (Code_Evaluation.Const (STR ''String.Char'') TYPEREP(num \<Rightarrow> char)) (t ())))
- (min (i - 1) 8) (* generate at most 8 bits *)
+ (min (i - 1) 8) \<comment> \<open>generate at most 8 bits\<close>
else None)"
instance ..
--- 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 */
--- 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 *)
--- 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
--- 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 ||
--- 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))))))
+ }
}
}
--- 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 ||
--- 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>\<open>theory_text\<close> (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"
--- 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";
--- 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 |--
--- 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,