--- a/NEWS Wed Nov 04 23:27:00 2015 +0100
+++ b/NEWS Thu Nov 05 00:02:30 2015 +0100
@@ -22,6 +22,10 @@
* Toplevel theorem statement 'proposition' is another alias for
'theorem'.
+* Syntax for formal comments "-- text" now also supports the symbolic
+form "\<comment> text". Command-line tool "isabelle update_cartouches -c" helps
+to update old sources.
+
*** Prover IDE -- Isabelle/Scala/jEdit ***
--- a/etc/symbols Wed Nov 04 23:27:00 2015 +0100
+++ b/etc/symbols Thu Nov 05 00:02:30 2015 +0100
@@ -348,6 +348,7 @@
\<some> code: 0x0003f5
\<hole> code: 0x002311
\<newline> code: 0x0023ce
+\<comment> code: 0x002015
\<open> code: 0x002039 group: punctuation font: IsabelleText abbrev: <<
\<close> code: 0x00203a group: punctuation font: IsabelleText abbrev: >>
\<here> code: 0x002302 font: IsabelleText
--- a/lib/Tools/update_cartouches Wed Nov 04 23:27:00 2015 +0100
+++ b/lib/Tools/update_cartouches Thu Nov 05 00:02:30 2015 +0100
@@ -15,6 +15,7 @@
echo "Usage: isabelle $PRG [FILES|DIRS...]"
echo
echo " Options are:"
+ echo " -c replace comment marker \"--\" by symbol \"\\<comment>\""
echo " -t replace @{text} antiquotations within text tokens"
echo
echo " Recursively find .thy files and update theory syntax to use cartouches"
@@ -30,11 +31,15 @@
# options
+COMMENT="false"
TEXT="false"
-while getopts "t" OPT
+while getopts "ct" OPT
do
case "$OPT" in
+ c)
+ COMMENT="true"
+ ;;
t)
TEXT="true"
;;
@@ -57,4 +62,4 @@
## main
find $SPECS -name \*.thy -print0 | \
- xargs -0 "$ISABELLE_TOOL" java isabelle.Update_Cartouches "$TEXT"
+ xargs -0 "$ISABELLE_TOOL" java isabelle.Update_Cartouches "$COMMENT" "$TEXT"
--- a/lib/texinputs/isabellesym.sty Wed Nov 04 23:27:00 2015 +0100
+++ b/lib/texinputs/isabellesym.sty Thu Nov 05 00:02:30 2015 +0100
@@ -358,3 +358,4 @@
\newcommand{\isasymclose}{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\rangle$}}}
\newcommand{\isasymhole}{\isatext{\rm\wasylozenge}} %requires wasysym
\newcommand{\isasymnewline}{\isatext{\fbox{$\hookleftarrow$}}}
+\newcommand{\isasymcomment}{\isatext{---}}
--- a/src/Doc/Isar_Ref/Outer_Syntax.thy Wed Nov 04 23:27:00 2015 +0100
+++ b/src/Doc/Isar_Ref/Outer_Syntax.thy Thu Nov 05 00:02:30 2015 +0100
@@ -223,17 +223,18 @@
subsection \<open>Comments \label{sec:comments}\<close>
-text \<open>Large chunks of plain @{syntax text} are usually given @{syntax
- verbatim}, i.e.\ enclosed in \<^verbatim>\<open>{*\<close>~\<open>\<dots>\<close>~\<^verbatim>\<open>*}\<close>,
- or as @{syntax cartouche} \<open>\<open>\<dots>\<close>\<close>. For convenience, any of the
- smaller text units conforming to @{syntax nameref} are admitted as well. A
- marginal @{syntax comment} is of the form \<^verbatim>\<open>--\<close>~@{syntax text}.
- Any number of these may occur within Isabelle/Isar commands.
+text \<open>
+ Large chunks of plain @{syntax text} are usually given @{syntax verbatim},
+ i.e.\ enclosed in \<^verbatim>\<open>{*\<close>~\<open>\<dots>\<close>~\<^verbatim>\<open>*}\<close>, or as @{syntax cartouche} \<open>\<open>\<dots>\<close>\<close>. For
+ convenience, any of the smaller text units conforming to @{syntax nameref}
+ are admitted as well. A marginal @{syntax comment} is of the form
+ \<^verbatim>\<open>--\<close>~@{syntax text} or \<^verbatim>\<open>\<comment>\<close>~@{syntax text}. Any number of these may occur
+ within Isabelle/Isar commands.
@{rail \<open>
@{syntax_def text}: @{syntax verbatim} | @{syntax cartouche} | @{syntax nameref}
;
- @{syntax_def comment}: '--' @{syntax text}
+ @{syntax_def comment}: ('--' | @'\<comment>') @{syntax text}
\<close>}
\<close>
--- a/src/Pure/General/symbol.ML Wed Nov 04 23:27:00 2015 +0100
+++ b/src/Pure/General/symbol.ML Thu Nov 05 00:02:30 2015 +0100
@@ -10,6 +10,7 @@
val STX: symbol
val DEL: symbol
val space: symbol
+ val comment: symbol
val is_char: symbol -> bool
val is_utf8: symbol -> bool
val is_symbolic: symbol -> bool
@@ -93,6 +94,8 @@
val space = chr 32;
+val comment = "\\<comment>";
+
fun is_char s = size s = 1;
fun is_utf8 s = size s > 0 andalso forall_string (fn c => ord c >= 128) s;
--- a/src/Pure/General/symbol.scala Wed Nov 04 23:27:00 2015 +0100
+++ b/src/Pure/General/symbol.scala Thu Nov 05 00:02:30 2015 +0100
@@ -433,6 +433,11 @@
val symbolic = recode_set((for { (sym, _) <- symbols; if raw_symbolic(sym) } yield sym): _*)
+ /* comment */
+
+ val comment_decoded = decode(comment)
+
+
/* cartouches */
val open_decoded = decode(open)
@@ -496,10 +501,16 @@
def is_blank(sym: Symbol): Boolean = symbols.blanks.contains(sym)
+ /* comment */
+
+ val comment: Symbol = "\\<comment>"
+ def comment_decoded: Symbol = symbols.comment_decoded
+
+
/* cartouches */
- val open = "\\<open>"
- val close = "\\<close>"
+ val open: Symbol = "\\<open>"
+ val close: Symbol = "\\<close>"
def open_decoded: Symbol = symbols.open_decoded
def close_decoded: Symbol = symbols.close_decoded
--- a/src/Pure/Isar/outer_syntax.ML Wed Nov 04 23:27:00 2015 +0100
+++ b/src/Pure/Isar/outer_syntax.ML Thu Nov 05 00:02:30 2015 +0100
@@ -197,7 +197,7 @@
in msg ^ quote (Markup.markup Markup.keyword1 name) end))
end);
-val parse_cmt = Parse.$$$ "--" -- Parse.!!! Parse.document_source;
+val parse_cmt = (Parse.$$$ "--" || Parse.$$$ Symbol.comment) -- Parse.!!! Parse.document_source;
fun commands_source thy =
Token.source_proper #>
@@ -261,7 +261,7 @@
(* side-comments *)
fun cmts (t1 :: t2 :: toks) =
- if Token.keyword_with (fn s => s = "--") t1 then t2 :: cmts toks
+ if Token.keyword_with (fn s => s = "--" orelse s = Symbol.comment) t1 then t2 :: cmts toks
else cmts (t2 :: toks)
| cmts _ = [];
--- a/src/Pure/PIDE/command.scala Wed Nov 04 23:27:00 2015 +0100
+++ b/src/Pure/PIDE/command.scala Thu Nov 05 00:02:30 2015 +0100
@@ -308,10 +308,11 @@
private def clean_tokens(tokens: List[Token]): List[(Token, Int)] =
{
+ val markers = Set("%", "--", Symbol.comment, Symbol.comment_decoded)
def clean(toks: List[(Token, Int)]): List[(Token, Int)] =
toks match {
case (t1, i1) :: (t2, i2) :: rest =>
- if (t1.is_keyword && (t1.source == "%" || t1.source == "--")) clean(rest)
+ if (t1.is_keyword && markers(t1.source)) clean(rest)
else (t1, i1) :: clean((t2, i2) :: rest)
case _ => toks
}
--- a/src/Pure/Pure.thy Wed Nov 04 23:27:00 2015 +0100
+++ b/src/Pure/Pure.thy Thu Nov 05 00:02:30 2015 +0100
@@ -6,7 +6,7 @@
theory Pure
keywords
- "!!" "!" "+" "--" ":" ";" "<" "<=" "=" "=>" "?" "[" "\<equiv>"
+ "!!" "!" "+" "--" ":" ";" "<" "<=" "=" "=>" "?" "[" "\<comment>" "\<equiv>"
"\<leftharpoondown>" "\<rightharpoonup>" "\<rightleftharpoons>"
"\<subseteq>" "]" "assumes" "attach" "binder" "constrains"
"defines" "fixes" "for" "identifier" "if" "in" "includes" "infix"
--- a/src/Pure/System/options.scala Wed Nov 04 23:27:00 2015 +0100
+++ b/src/Pure/System/options.scala Thu Nov 05 00:02:30 2015 +0100
@@ -75,7 +75,7 @@
private val PREFS = PREFS_DIR + Path.basic("preferences")
lazy val options_syntax =
- Outer_Syntax.init() + ":" + "=" + "--" +
+ Outer_Syntax.init() + ":" + "=" + "--" + Symbol.comment + Symbol.comment_decoded +
(SECTION, Keyword.DOCUMENT_HEADING) + PUBLIC + (OPTION, Keyword.THY_DECL)
lazy val prefs_syntax = Outer_Syntax.init() + "="
@@ -89,12 +89,15 @@
{ case s ~ n => if (s.isDefined) "-" + n else n } |
atom("option value", tok => tok.is_name || tok.is_float)
+ def comment_marker: Parser[String] =
+ $$$("--") | $$$(Symbol.comment) | $$$(Symbol.comment_decoded)
+
val option_entry: Parser[Options => Options] =
{
command(SECTION) ~! text ^^
{ case _ ~ a => (options: Options) => options.set_section(a) } |
opt($$$(PUBLIC)) ~ command(OPTION) ~! (position(option_name) ~ $$$(":") ~ option_type ~
- $$$("=") ~ option_value ~ ($$$("--") ~! text ^^ { case _ ~ x => x } | success(""))) ^^
+ $$$("=") ~ option_value ~ (comment_marker ~! text ^^ { case _ ~ x => x } | success(""))) ^^
{ case a ~ _ ~ ((b, pos) ~ _ ~ c ~ _ ~ d ~ e) =>
(options: Options) => options.declare(a.isDefined, pos, b, c, d, e) }
}
--- a/src/Pure/Thy/thy_output.ML Wed Nov 04 23:27:00 2015 +0100
+++ b/src/Pure/Thy/thy_output.ML Thu Nov 05 00:02:30 2015 +0100
@@ -430,7 +430,8 @@
(Basic_Token cmd, (markup_false, d)))]));
val cmt = Scan.peek (fn d =>
- Parse.$$$ "--" |-- Parse.!!!! (improper |-- Parse.document_source) >>
+ (Parse.$$$ "--" || Parse.$$$ Symbol.comment) |--
+ Parse.!!!! (improper |-- Parse.document_source) >>
(fn source => (NONE, (Markup_Token ("cmt", source), ("", d)))));
val other = Scan.peek (fn d =>
--- a/src/Pure/Tools/update_cartouches.scala Wed Nov 04 23:27:00 2015 +0100
+++ b/src/Pure/Tools/update_cartouches.scala Thu Nov 05 00:02:30 2015 +0100
@@ -1,7 +1,7 @@
/* Title: Pure/Tools/update_cartouches.scala
Author: Makarius
-Update theory syntax to use cartouches.
+Update theory syntax to use cartouches etc.
*/
package isabelle
@@ -37,11 +37,11 @@
}
}
- def update_cartouches(replace_text: Boolean, path: Path)
+ def update_cartouches(replace_comment: Boolean, replace_text: Boolean, path: Path)
{
val text0 = File.read(path)
- // outer syntax cartouches
+ // outer syntax cartouches and comment markers
val text1 =
(for (tok <- Token.explode(Keyword.Keywords.empty, text0).iterator)
yield {
@@ -52,6 +52,7 @@
case s => tok.source
}
}
+ else if (replace_comment && tok.source == "--") Symbol.comment
else tok.source
}
).mkString
@@ -87,8 +88,10 @@
{
Command_Line.tool0 {
args.toList match {
- case Properties.Value.Boolean(replace_text) :: files =>
- files.foreach(file => update_cartouches(replace_text, Path.explode(file)))
+ case Properties.Value.Boolean(replace_comment) ::
+ Properties.Value.Boolean(replace_text) :: files =>
+ files.foreach(file =>
+ update_cartouches(replace_comment, replace_text, Path.explode(file)))
case _ => error("Bad arguments:\n" + cat_lines(args))
}
}
--- a/src/Tools/jEdit/src/rendering.scala Wed Nov 04 23:27:00 2015 +0100
+++ b/src/Tools/jEdit/src/rendering.scala Thu Nov 05 00:02:30 2015 +0100
@@ -94,6 +94,7 @@
def token_markup(syntax: Outer_Syntax, token: Token): Byte =
if (token.is_command) command_style(syntax.keywords.command_kind(token.content).getOrElse(""))
+ else if (token.is_keyword && token.source == Symbol.comment_decoded) JEditToken.NULL
else if (token.is_delimiter) JEditToken.OPERATOR
else token_style(token.kind)