# HG changeset patch # User wenzelm # Date 1446678150 -3600 # Node ID 634cd44bb1d3dd13baae8beb239c3143e1556c61 # Parent 6623c81cb15a48477d6d454d457a1d9c3f17dcb9 symbolic syntax "\ text"; diff -r 6623c81cb15a -r 634cd44bb1d3 NEWS --- 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 "\ text". Command-line tool "isabelle update_cartouches -c" helps +to update old sources. + *** Prover IDE -- Isabelle/Scala/jEdit *** diff -r 6623c81cb15a -r 634cd44bb1d3 etc/symbols --- 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 @@ \ code: 0x0003f5 \ code: 0x002311 \ code: 0x0023ce +\ code: 0x002015 \ code: 0x002039 group: punctuation font: IsabelleText abbrev: << \ code: 0x00203a group: punctuation font: IsabelleText abbrev: >> \ code: 0x002302 font: IsabelleText diff -r 6623c81cb15a -r 634cd44bb1d3 lib/Tools/update_cartouches --- 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 \"\\\"" 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" diff -r 6623c81cb15a -r 634cd44bb1d3 lib/texinputs/isabellesym.sty --- 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{---}} diff -r 6623c81cb15a -r 634cd44bb1d3 src/Doc/Isar_Ref/Outer_Syntax.thy --- 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 \Comments \label{sec:comments}\ -text \Large chunks of plain @{syntax text} are usually given @{syntax - verbatim}, i.e.\ enclosed in \<^verbatim>\{*\~\\\~\<^verbatim>\*}\, - or as @{syntax cartouche} \\\\\. 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>\--\~@{syntax text}. - Any number of these may occur within Isabelle/Isar commands. +text \ + Large chunks of plain @{syntax text} are usually given @{syntax verbatim}, + i.e.\ enclosed in \<^verbatim>\{*\~\\\~\<^verbatim>\*}\, or as @{syntax cartouche} \\\\\. 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>\--\~@{syntax text} or \<^verbatim>\\\~@{syntax text}. Any number of these may occur + within Isabelle/Isar commands. @{rail \ @{syntax_def text}: @{syntax verbatim} | @{syntax cartouche} | @{syntax nameref} ; - @{syntax_def comment}: '--' @{syntax text} + @{syntax_def comment}: ('--' | @'\') @{syntax text} \} \ diff -r 6623c81cb15a -r 634cd44bb1d3 src/Pure/General/symbol.ML --- 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 = "\\"; + fun is_char s = size s = 1; fun is_utf8 s = size s > 0 andalso forall_string (fn c => ord c >= 128) s; diff -r 6623c81cb15a -r 634cd44bb1d3 src/Pure/General/symbol.scala --- 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 = "\\" + def comment_decoded: Symbol = symbols.comment_decoded + + /* cartouches */ - val open = "\\" - val close = "\\" + val open: Symbol = "\\" + val close: Symbol = "\\" def open_decoded: Symbol = symbols.open_decoded def close_decoded: Symbol = symbols.close_decoded diff -r 6623c81cb15a -r 634cd44bb1d3 src/Pure/Isar/outer_syntax.ML --- 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 _ = []; diff -r 6623c81cb15a -r 634cd44bb1d3 src/Pure/PIDE/command.scala --- 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 } diff -r 6623c81cb15a -r 634cd44bb1d3 src/Pure/Pure.thy --- 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 - "!!" "!" "+" "--" ":" ";" "<" "<=" "=" "=>" "?" "[" "\" + "!!" "!" "+" "--" ":" ";" "<" "<=" "=" "=>" "?" "[" "\" "\" "\" "\" "\" "\" "]" "assumes" "attach" "binder" "constrains" "defines" "fixes" "for" "identifier" "if" "in" "includes" "infix" diff -r 6623c81cb15a -r 634cd44bb1d3 src/Pure/System/options.scala --- 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) } } diff -r 6623c81cb15a -r 634cd44bb1d3 src/Pure/Thy/thy_output.ML --- 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 => diff -r 6623c81cb15a -r 634cd44bb1d3 src/Pure/Tools/update_cartouches.scala --- 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)) } } diff -r 6623c81cb15a -r 634cd44bb1d3 src/Tools/jEdit/src/rendering.scala --- 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)