# HG changeset patch
# User wenzelm
# Date 1515957011 -3600
# Node ID e0c0c1f0e3e797e8d072f0b31533239dedf84376
# Parent  e6d5547a0a9368e6503fafd49fcc4addff2d7165
more specific tool "isabelle update_comments", for uniformity with formal comments in embedded languages;

diff -r e6d5547a0a93 -r e0c0c1f0e3e7 NEWS
--- a/NEWS	Sun Jan 14 19:45:48 2018 +0100
+++ b/NEWS	Sun Jan 14 20:10:11 2018 +0100
@@ -212,6 +212,12 @@
 
 *** System ***
 
+* The command-line tool "isabelle update_comments" normalizes formal
+comments in outer syntax as follows: \<comment> \<open>text\<close> (whith a single space to
+approximate the appearance in document output). This is more specific
+than former "isabelle update_cartouches -c": the latter tool option has
+been discontinued.
+
 * Session ROOT entry: empty 'document_files' means there is no document
 for this session. There is no need to specify options [document = false]
 anymore.
diff -r e6d5547a0a93 -r e0c0c1f0e3e7 src/Pure/System/isabelle_tool.scala
--- a/src/Pure/System/isabelle_tool.scala	Sun Jan 14 19:45:48 2018 +0100
+++ b/src/Pure/System/isabelle_tool.scala	Sun Jan 14 20:10:11 2018 +0100
@@ -119,6 +119,7 @@
       Remote_DMG.isabelle_tool,
       Server.isabelle_tool,
       Update_Cartouches.isabelle_tool,
+      Update_Comments.isabelle_tool,
       Update_Header.isabelle_tool,
       Update_Then.isabelle_tool,
       Update_Theorems.isabelle_tool,
diff -r e6d5547a0a93 -r e0c0c1f0e3e7 src/Pure/Tools/update_cartouches.scala
--- a/src/Pure/Tools/update_cartouches.scala	Sun Jan 14 19:45:48 2018 +0100
+++ b/src/Pure/Tools/update_cartouches.scala	Sun Jan 14 20:10:11 2018 +0100
@@ -34,11 +34,11 @@
     }
   }
 
-  def update_cartouches(replace_comment: Boolean, replace_text: Boolean, path: Path)
+  def update_cartouches(replace_text: Boolean, path: Path)
   {
     val text0 = File.read(path)
 
-    // outer syntax cartouches and comment markers
+    // outer syntax cartouches
     val text1 =
       (for (tok <- Token.explode(Keyword.Keywords.empty, text0).iterator)
         yield {
@@ -49,7 +49,6 @@
               case s => tok.source
             }
           }
-          else if (replace_comment && tok.source == "--") Symbol.comment
           else tok.source
         }
       ).mkString
@@ -84,14 +83,12 @@
   val isabelle_tool =
     Isabelle_Tool("update_cartouches", "update theory syntax to use cartouches", args =>
     {
-      var replace_comment = false
       var replace_text = false
 
       val getopts = Getopts("""
 Usage: isabelle update_cartouches [FILES|DIRS...]
 
   Options are:
-    -c           replace comment marker "--" by symbol "\<comment>"
     -t           replace @{text} antiquotations within text tokens
 
   Recursively find .thy files and update theory syntax to use cartouches
@@ -99,7 +96,6 @@
 
   Old versions of files are preserved by appending "~~".
 """,
-        "c" -> (_ => replace_comment = true),
         "t" -> (_ => replace_text = true))
 
       val specs = getopts(args)
@@ -108,6 +104,6 @@
       for {
         spec <- specs
         file <- File.find_files(Path.explode(spec).file, file => file.getName.endsWith(".thy"))
-      } update_cartouches(replace_comment, replace_text, Path.explode(File.standard_path(file)))
+      } update_cartouches(replace_text, Path.explode(File.standard_path(file)))
     })
 }
diff -r e6d5547a0a93 -r e0c0c1f0e3e7 src/Pure/Tools/update_comments.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Tools/update_comments.scala	Sun Jan 14 20:10:11 2018 +0100
@@ -0,0 +1,63 @@
+/*  Title:      Pure/Tools/update_comments.scala
+    Author:     Makarius
+
+Update formal comments in outer syntax: \<comment> \<open>...\<close>
+*/
+
+package isabelle
+
+
+import scala.annotation.tailrec
+
+
+object Update_Comments
+{
+  def update_comments(path: Path)
+  {
+    @tailrec def update(toks: List[Token], result: List[String]): String =
+    {
+      toks match {
+        case tok :: rest if tok.source == "--" || tok.source == Symbol.comment =>
+          rest.dropWhile(_.is_space) match {
+            case tok1 :: rest1 if tok1.is_text =>
+              val res = Symbol.comment + Symbol.space + Library.cartouche(tok1.content)
+              update(rest1, res :: result)
+            case _ => update(rest, tok.source :: result)
+          }
+        case tok :: rest => update(rest, tok.source :: result)
+        case Nil => result.reverse.mkString
+      }
+    }
+
+    val text0 = File.read(path)
+    val text1 = update(Token.explode(Keyword.Keywords.empty, text0), Nil)
+
+    if (text0 != text1) {
+      Output.writeln("changing " + path)
+      File.write_backup2(path, text1)
+    }
+  }
+
+
+  /* Isabelle tool wrapper */
+
+  val isabelle_tool =
+    Isabelle_Tool("update_comments", "update formal comments in outer syntax", args =>
+    {
+      val getopts = Getopts("""
+Usage: isabelle update_comments [FILES|DIRS...]
+
+  Recursively find .thy files and update formal comments in outer syntax.
+
+  Old versions of files are preserved by appending "~~".
+""")
+
+      val specs = getopts(args)
+      if (specs.isEmpty) getopts.usage()
+
+      for {
+        spec <- specs
+        file <- File.find_files(Path.explode(spec).file, file => file.getName.endsWith(".thy"))
+      } update_comments(Path.explode(File.standard_path(file)))
+    })
+}
diff -r e6d5547a0a93 -r e0c0c1f0e3e7 src/Pure/build-jars
--- a/src/Pure/build-jars	Sun Jan 14 19:45:48 2018 +0100
+++ b/src/Pure/build-jars	Sun Jan 14 20:10:11 2018 +0100
@@ -148,6 +148,7 @@
   Tools/spell_checker.scala
   Tools/task_statistics.scala
   Tools/update_cartouches.scala
+  Tools/update_comments.scala
   Tools/update_header.scala
   Tools/update_then.scala
   Tools/update_theorems.scala