symbolic syntax "\<comment> text";
authorwenzelm
Thu, 05 Nov 2015 00:02:30 +0100
changeset 61579 634cd44bb1d3
parent 61578 6623c81cb15a
child 61580 c49a8ebd30cc
symbolic syntax "\<comment> text";
NEWS
etc/symbols
lib/Tools/update_cartouches
lib/texinputs/isabellesym.sty
src/Doc/Isar_Ref/Outer_Syntax.thy
src/Pure/General/symbol.ML
src/Pure/General/symbol.scala
src/Pure/Isar/outer_syntax.ML
src/Pure/PIDE/command.scala
src/Pure/Pure.thy
src/Pure/System/options.scala
src/Pure/Thy/thy_output.ML
src/Pure/Tools/update_cartouches.scala
src/Tools/jEdit/src/rendering.scala
--- 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)