symbolic syntax "\<comment> text";
authorwenzelm
Thu Nov 05 00:02:30 2015 +0100 (2015-11-05)
changeset 61579634cd44bb1d3
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
     1.1 --- a/NEWS	Wed Nov 04 23:27:00 2015 +0100
     1.2 +++ b/NEWS	Thu Nov 05 00:02:30 2015 +0100
     1.3 @@ -22,6 +22,10 @@
     1.4  * Toplevel theorem statement 'proposition' is another alias for
     1.5  'theorem'.
     1.6  
     1.7 +* Syntax for formal comments "-- text" now also supports the symbolic
     1.8 +form "\<comment> text". Command-line tool "isabelle update_cartouches -c" helps
     1.9 +to update old sources.
    1.10 +
    1.11  
    1.12  *** Prover IDE -- Isabelle/Scala/jEdit ***
    1.13  
     2.1 --- a/etc/symbols	Wed Nov 04 23:27:00 2015 +0100
     2.2 +++ b/etc/symbols	Thu Nov 05 00:02:30 2015 +0100
     2.3 @@ -348,6 +348,7 @@
     2.4  \<some>                 code: 0x0003f5
     2.5  \<hole>                 code: 0x002311
     2.6  \<newline>              code: 0x0023ce
     2.7 +\<comment>              code: 0x002015
     2.8  \<open>                 code: 0x002039  group: punctuation  font: IsabelleText  abbrev: <<
     2.9  \<close>                code: 0x00203a  group: punctuation  font: IsabelleText  abbrev: >>
    2.10  \<here>                 code: 0x002302  font: IsabelleText
     3.1 --- a/lib/Tools/update_cartouches	Wed Nov 04 23:27:00 2015 +0100
     3.2 +++ b/lib/Tools/update_cartouches	Thu Nov 05 00:02:30 2015 +0100
     3.3 @@ -15,6 +15,7 @@
     3.4    echo "Usage: isabelle $PRG [FILES|DIRS...]"
     3.5    echo
     3.6    echo "  Options are:"
     3.7 +  echo "    -c           replace comment marker \"--\" by symbol \"\\<comment>\""
     3.8    echo "    -t           replace @{text} antiquotations within text tokens"
     3.9    echo
    3.10    echo "  Recursively find .thy files and update theory syntax to use cartouches"
    3.11 @@ -30,11 +31,15 @@
    3.12  
    3.13  # options
    3.14  
    3.15 +COMMENT="false"
    3.16  TEXT="false"
    3.17  
    3.18 -while getopts "t" OPT
    3.19 +while getopts "ct" OPT
    3.20  do
    3.21    case "$OPT" in
    3.22 +    c)
    3.23 +      COMMENT="true"
    3.24 +      ;;
    3.25      t)
    3.26        TEXT="true"
    3.27        ;;
    3.28 @@ -57,4 +62,4 @@
    3.29  ## main
    3.30  
    3.31  find $SPECS -name \*.thy -print0 | \
    3.32 -  xargs -0 "$ISABELLE_TOOL" java isabelle.Update_Cartouches "$TEXT"
    3.33 +  xargs -0 "$ISABELLE_TOOL" java isabelle.Update_Cartouches "$COMMENT" "$TEXT"
     4.1 --- a/lib/texinputs/isabellesym.sty	Wed Nov 04 23:27:00 2015 +0100
     4.2 +++ b/lib/texinputs/isabellesym.sty	Thu Nov 05 00:02:30 2015 +0100
     4.3 @@ -358,3 +358,4 @@
     4.4  \newcommand{\isasymclose}{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\rangle$}}}
     4.5  \newcommand{\isasymhole}{\isatext{\rm\wasylozenge}}  %requires wasysym
     4.6  \newcommand{\isasymnewline}{\isatext{\fbox{$\hookleftarrow$}}}
     4.7 +\newcommand{\isasymcomment}{\isatext{---}}
     5.1 --- a/src/Doc/Isar_Ref/Outer_Syntax.thy	Wed Nov 04 23:27:00 2015 +0100
     5.2 +++ b/src/Doc/Isar_Ref/Outer_Syntax.thy	Thu Nov 05 00:02:30 2015 +0100
     5.3 @@ -223,17 +223,18 @@
     5.4  
     5.5  subsection \<open>Comments \label{sec:comments}\<close>
     5.6  
     5.7 -text \<open>Large chunks of plain @{syntax text} are usually given @{syntax
     5.8 -  verbatim}, i.e.\ enclosed in \<^verbatim>\<open>{*\<close>~\<open>\<dots>\<close>~\<^verbatim>\<open>*}\<close>,
     5.9 -  or as @{syntax cartouche} \<open>\<open>\<dots>\<close>\<close>. For convenience, any of the
    5.10 -  smaller text units conforming to @{syntax nameref} are admitted as well. A
    5.11 -  marginal @{syntax comment} is of the form \<^verbatim>\<open>--\<close>~@{syntax text}.
    5.12 -  Any number of these may occur within Isabelle/Isar commands.
    5.13 +text \<open>
    5.14 +  Large chunks of plain @{syntax text} are usually given @{syntax verbatim},
    5.15 +  i.e.\ enclosed in \<^verbatim>\<open>{*\<close>~\<open>\<dots>\<close>~\<^verbatim>\<open>*}\<close>, or as @{syntax cartouche} \<open>\<open>\<dots>\<close>\<close>. For
    5.16 +  convenience, any of the smaller text units conforming to @{syntax nameref}
    5.17 +  are admitted as well. A marginal @{syntax comment} is of the form
    5.18 +  \<^verbatim>\<open>--\<close>~@{syntax text} or \<^verbatim>\<open>\<comment>\<close>~@{syntax text}. Any number of these may occur
    5.19 +  within Isabelle/Isar commands.
    5.20  
    5.21    @{rail \<open>
    5.22      @{syntax_def text}: @{syntax verbatim} | @{syntax cartouche} | @{syntax nameref}
    5.23      ;
    5.24 -    @{syntax_def comment}: '--' @{syntax text}
    5.25 +    @{syntax_def comment}: ('--' | @'\<comment>') @{syntax text}
    5.26    \<close>}
    5.27  \<close>
    5.28  
     6.1 --- a/src/Pure/General/symbol.ML	Wed Nov 04 23:27:00 2015 +0100
     6.2 +++ b/src/Pure/General/symbol.ML	Thu Nov 05 00:02:30 2015 +0100
     6.3 @@ -10,6 +10,7 @@
     6.4    val STX: symbol
     6.5    val DEL: symbol
     6.6    val space: symbol
     6.7 +  val comment: symbol
     6.8    val is_char: symbol -> bool
     6.9    val is_utf8: symbol -> bool
    6.10    val is_symbolic: symbol -> bool
    6.11 @@ -93,6 +94,8 @@
    6.12  
    6.13  val space = chr 32;
    6.14  
    6.15 +val comment = "\\<comment>";
    6.16 +
    6.17  fun is_char s = size s = 1;
    6.18  
    6.19  fun is_utf8 s = size s > 0 andalso forall_string (fn c => ord c >= 128) s;
     7.1 --- a/src/Pure/General/symbol.scala	Wed Nov 04 23:27:00 2015 +0100
     7.2 +++ b/src/Pure/General/symbol.scala	Thu Nov 05 00:02:30 2015 +0100
     7.3 @@ -433,6 +433,11 @@
     7.4      val symbolic = recode_set((for { (sym, _) <- symbols; if raw_symbolic(sym) } yield sym): _*)
     7.5  
     7.6  
     7.7 +    /* comment */
     7.8 +
     7.9 +    val comment_decoded = decode(comment)
    7.10 +
    7.11 +
    7.12      /* cartouches */
    7.13  
    7.14      val open_decoded = decode(open)
    7.15 @@ -496,10 +501,16 @@
    7.16    def is_blank(sym: Symbol): Boolean = symbols.blanks.contains(sym)
    7.17  
    7.18  
    7.19 +  /* comment */
    7.20 +
    7.21 +  val comment: Symbol = "\\<comment>"
    7.22 +  def comment_decoded: Symbol = symbols.comment_decoded
    7.23 +
    7.24 +
    7.25    /* cartouches */
    7.26  
    7.27 -  val open = "\\<open>"
    7.28 -  val close = "\\<close>"
    7.29 +  val open: Symbol = "\\<open>"
    7.30 +  val close: Symbol = "\\<close>"
    7.31  
    7.32    def open_decoded: Symbol = symbols.open_decoded
    7.33    def close_decoded: Symbol = symbols.close_decoded
     8.1 --- a/src/Pure/Isar/outer_syntax.ML	Wed Nov 04 23:27:00 2015 +0100
     8.2 +++ b/src/Pure/Isar/outer_syntax.ML	Thu Nov 05 00:02:30 2015 +0100
     8.3 @@ -197,7 +197,7 @@
     8.4              in msg ^ quote (Markup.markup Markup.keyword1 name) end))
     8.5      end);
     8.6  
     8.7 -val parse_cmt = Parse.$$$ "--" -- Parse.!!! Parse.document_source;
     8.8 +val parse_cmt = (Parse.$$$ "--" || Parse.$$$ Symbol.comment) -- Parse.!!! Parse.document_source;
     8.9  
    8.10  fun commands_source thy =
    8.11    Token.source_proper #>
    8.12 @@ -261,7 +261,7 @@
    8.13  (* side-comments *)
    8.14  
    8.15  fun cmts (t1 :: t2 :: toks) =
    8.16 -      if Token.keyword_with (fn s => s = "--") t1 then t2 :: cmts toks
    8.17 +      if Token.keyword_with (fn s => s = "--" orelse s = Symbol.comment) t1 then t2 :: cmts toks
    8.18        else cmts (t2 :: toks)
    8.19    | cmts _ = [];
    8.20  
     9.1 --- a/src/Pure/PIDE/command.scala	Wed Nov 04 23:27:00 2015 +0100
     9.2 +++ b/src/Pure/PIDE/command.scala	Thu Nov 05 00:02:30 2015 +0100
     9.3 @@ -308,10 +308,11 @@
     9.4  
     9.5    private def clean_tokens(tokens: List[Token]): List[(Token, Int)] =
     9.6    {
     9.7 +    val markers = Set("%", "--", Symbol.comment, Symbol.comment_decoded)
     9.8      def clean(toks: List[(Token, Int)]): List[(Token, Int)] =
     9.9        toks match {
    9.10          case (t1, i1) :: (t2, i2) :: rest =>
    9.11 -          if (t1.is_keyword && (t1.source == "%" || t1.source == "--")) clean(rest)
    9.12 +          if (t1.is_keyword && markers(t1.source)) clean(rest)
    9.13            else (t1, i1) :: clean((t2, i2) :: rest)
    9.14          case _ => toks
    9.15        }
    10.1 --- a/src/Pure/Pure.thy	Wed Nov 04 23:27:00 2015 +0100
    10.2 +++ b/src/Pure/Pure.thy	Thu Nov 05 00:02:30 2015 +0100
    10.3 @@ -6,7 +6,7 @@
    10.4  
    10.5  theory Pure
    10.6    keywords
    10.7 -    "!!" "!" "+" "--" ":" ";" "<" "<=" "=" "=>" "?" "[" "\<equiv>"
    10.8 +    "!!" "!" "+" "--" ":" ";" "<" "<=" "=" "=>" "?" "[" "\<comment>" "\<equiv>"
    10.9      "\<leftharpoondown>" "\<rightharpoonup>" "\<rightleftharpoons>"
   10.10      "\<subseteq>" "]" "assumes" "attach" "binder" "constrains"
   10.11      "defines" "fixes" "for" "identifier" "if" "in" "includes" "infix"
    11.1 --- a/src/Pure/System/options.scala	Wed Nov 04 23:27:00 2015 +0100
    11.2 +++ b/src/Pure/System/options.scala	Thu Nov 05 00:02:30 2015 +0100
    11.3 @@ -75,7 +75,7 @@
    11.4    private val PREFS = PREFS_DIR + Path.basic("preferences")
    11.5  
    11.6    lazy val options_syntax =
    11.7 -    Outer_Syntax.init() + ":" + "=" + "--" +
    11.8 +    Outer_Syntax.init() + ":" + "=" + "--" + Symbol.comment + Symbol.comment_decoded +
    11.9        (SECTION, Keyword.DOCUMENT_HEADING) + PUBLIC + (OPTION, Keyword.THY_DECL)
   11.10  
   11.11    lazy val prefs_syntax = Outer_Syntax.init() + "="
   11.12 @@ -89,12 +89,15 @@
   11.13          { case s ~ n => if (s.isDefined) "-" + n else n } |
   11.14        atom("option value", tok => tok.is_name || tok.is_float)
   11.15  
   11.16 +    def comment_marker: Parser[String] =
   11.17 +      $$$("--") | $$$(Symbol.comment) | $$$(Symbol.comment_decoded)
   11.18 +
   11.19      val option_entry: Parser[Options => Options] =
   11.20      {
   11.21        command(SECTION) ~! text ^^
   11.22          { case _ ~ a => (options: Options) => options.set_section(a) } |
   11.23        opt($$$(PUBLIC)) ~ command(OPTION) ~! (position(option_name) ~ $$$(":") ~ option_type ~
   11.24 -      $$$("=") ~ option_value ~ ($$$("--") ~! text ^^ { case _ ~ x => x } | success(""))) ^^
   11.25 +      $$$("=") ~ option_value ~ (comment_marker ~! text ^^ { case _ ~ x => x } | success(""))) ^^
   11.26          { case a ~ _ ~ ((b, pos) ~ _ ~ c ~ _ ~ d ~ e) =>
   11.27              (options: Options) => options.declare(a.isDefined, pos, b, c, d, e) }
   11.28      }
    12.1 --- a/src/Pure/Thy/thy_output.ML	Wed Nov 04 23:27:00 2015 +0100
    12.2 +++ b/src/Pure/Thy/thy_output.ML	Thu Nov 05 00:02:30 2015 +0100
    12.3 @@ -430,7 +430,8 @@
    12.4              (Basic_Token cmd, (markup_false, d)))]));
    12.5  
    12.6      val cmt = Scan.peek (fn d =>
    12.7 -      Parse.$$$ "--" |-- Parse.!!!! (improper |-- Parse.document_source) >>
    12.8 +      (Parse.$$$ "--" || Parse.$$$ Symbol.comment) |--
    12.9 +        Parse.!!!! (improper |-- Parse.document_source) >>
   12.10          (fn source => (NONE, (Markup_Token ("cmt", source), ("", d)))));
   12.11  
   12.12      val other = Scan.peek (fn d =>
    13.1 --- a/src/Pure/Tools/update_cartouches.scala	Wed Nov 04 23:27:00 2015 +0100
    13.2 +++ b/src/Pure/Tools/update_cartouches.scala	Thu Nov 05 00:02:30 2015 +0100
    13.3 @@ -1,7 +1,7 @@
    13.4  /*  Title:      Pure/Tools/update_cartouches.scala
    13.5      Author:     Makarius
    13.6  
    13.7 -Update theory syntax to use cartouches.
    13.8 +Update theory syntax to use cartouches etc.
    13.9  */
   13.10  
   13.11  package isabelle
   13.12 @@ -37,11 +37,11 @@
   13.13      }
   13.14    }
   13.15  
   13.16 -  def update_cartouches(replace_text: Boolean, path: Path)
   13.17 +  def update_cartouches(replace_comment: Boolean, replace_text: Boolean, path: Path)
   13.18    {
   13.19      val text0 = File.read(path)
   13.20  
   13.21 -    // outer syntax cartouches
   13.22 +    // outer syntax cartouches and comment markers
   13.23      val text1 =
   13.24        (for (tok <- Token.explode(Keyword.Keywords.empty, text0).iterator)
   13.25          yield {
   13.26 @@ -52,6 +52,7 @@
   13.27                case s => tok.source
   13.28              }
   13.29            }
   13.30 +          else if (replace_comment && tok.source == "--") Symbol.comment
   13.31            else tok.source
   13.32          }
   13.33        ).mkString
   13.34 @@ -87,8 +88,10 @@
   13.35    {
   13.36      Command_Line.tool0 {
   13.37        args.toList match {
   13.38 -        case Properties.Value.Boolean(replace_text) :: files =>
   13.39 -          files.foreach(file => update_cartouches(replace_text, Path.explode(file)))
   13.40 +        case Properties.Value.Boolean(replace_comment) ::
   13.41 +            Properties.Value.Boolean(replace_text) :: files =>
   13.42 +          files.foreach(file =>
   13.43 +            update_cartouches(replace_comment, replace_text, Path.explode(file)))
   13.44          case _ => error("Bad arguments:\n" + cat_lines(args))
   13.45        }
   13.46      }
    14.1 --- a/src/Tools/jEdit/src/rendering.scala	Wed Nov 04 23:27:00 2015 +0100
    14.2 +++ b/src/Tools/jEdit/src/rendering.scala	Thu Nov 05 00:02:30 2015 +0100
    14.3 @@ -94,6 +94,7 @@
    14.4  
    14.5    def token_markup(syntax: Outer_Syntax, token: Token): Byte =
    14.6      if (token.is_command) command_style(syntax.keywords.command_kind(token.content).getOrElse(""))
    14.7 +    else if (token.is_keyword && token.source == Symbol.comment_decoded) JEditToken.NULL
    14.8      else if (token.is_delimiter) JEditToken.OPERATOR
    14.9      else token_style(token.kind)
   14.10