more specific tool "isabelle update_comments", for uniformity with formal comments in embedded languages;
authorwenzelm
Sun Jan 14 20:10:11 2018 +0100 (17 months ago)
changeset 67433e0c0c1f0e3e7
parent 67432 e6d5547a0a93
child 67434 a38c74b0886d
more specific tool "isabelle update_comments", for uniformity with formal comments in embedded languages;
NEWS
src/Pure/System/isabelle_tool.scala
src/Pure/Tools/update_cartouches.scala
src/Pure/Tools/update_comments.scala
src/Pure/build-jars
     1.1 --- a/NEWS	Sun Jan 14 19:45:48 2018 +0100
     1.2 +++ b/NEWS	Sun Jan 14 20:10:11 2018 +0100
     1.3 @@ -212,6 +212,12 @@
     1.4  
     1.5  *** System ***
     1.6  
     1.7 +* The command-line tool "isabelle update_comments" normalizes formal
     1.8 +comments in outer syntax as follows: \<comment> \<open>text\<close> (whith a single space to
     1.9 +approximate the appearance in document output). This is more specific
    1.10 +than former "isabelle update_cartouches -c": the latter tool option has
    1.11 +been discontinued.
    1.12 +
    1.13  * Session ROOT entry: empty 'document_files' means there is no document
    1.14  for this session. There is no need to specify options [document = false]
    1.15  anymore.
     2.1 --- a/src/Pure/System/isabelle_tool.scala	Sun Jan 14 19:45:48 2018 +0100
     2.2 +++ b/src/Pure/System/isabelle_tool.scala	Sun Jan 14 20:10:11 2018 +0100
     2.3 @@ -119,6 +119,7 @@
     2.4        Remote_DMG.isabelle_tool,
     2.5        Server.isabelle_tool,
     2.6        Update_Cartouches.isabelle_tool,
     2.7 +      Update_Comments.isabelle_tool,
     2.8        Update_Header.isabelle_tool,
     2.9        Update_Then.isabelle_tool,
    2.10        Update_Theorems.isabelle_tool,
     3.1 --- a/src/Pure/Tools/update_cartouches.scala	Sun Jan 14 19:45:48 2018 +0100
     3.2 +++ b/src/Pure/Tools/update_cartouches.scala	Sun Jan 14 20:10:11 2018 +0100
     3.3 @@ -34,11 +34,11 @@
     3.4      }
     3.5    }
     3.6  
     3.7 -  def update_cartouches(replace_comment: Boolean, replace_text: Boolean, path: Path)
     3.8 +  def update_cartouches(replace_text: Boolean, path: Path)
     3.9    {
    3.10      val text0 = File.read(path)
    3.11  
    3.12 -    // outer syntax cartouches and comment markers
    3.13 +    // outer syntax cartouches
    3.14      val text1 =
    3.15        (for (tok <- Token.explode(Keyword.Keywords.empty, text0).iterator)
    3.16          yield {
    3.17 @@ -49,7 +49,6 @@
    3.18                case s => tok.source
    3.19              }
    3.20            }
    3.21 -          else if (replace_comment && tok.source == "--") Symbol.comment
    3.22            else tok.source
    3.23          }
    3.24        ).mkString
    3.25 @@ -84,14 +83,12 @@
    3.26    val isabelle_tool =
    3.27      Isabelle_Tool("update_cartouches", "update theory syntax to use cartouches", args =>
    3.28      {
    3.29 -      var replace_comment = false
    3.30        var replace_text = false
    3.31  
    3.32        val getopts = Getopts("""
    3.33  Usage: isabelle update_cartouches [FILES|DIRS...]
    3.34  
    3.35    Options are:
    3.36 -    -c           replace comment marker "--" by symbol "\<comment>"
    3.37      -t           replace @{text} antiquotations within text tokens
    3.38  
    3.39    Recursively find .thy files and update theory syntax to use cartouches
    3.40 @@ -99,7 +96,6 @@
    3.41  
    3.42    Old versions of files are preserved by appending "~~".
    3.43  """,
    3.44 -        "c" -> (_ => replace_comment = true),
    3.45          "t" -> (_ => replace_text = true))
    3.46  
    3.47        val specs = getopts(args)
    3.48 @@ -108,6 +104,6 @@
    3.49        for {
    3.50          spec <- specs
    3.51          file <- File.find_files(Path.explode(spec).file, file => file.getName.endsWith(".thy"))
    3.52 -      } update_cartouches(replace_comment, replace_text, Path.explode(File.standard_path(file)))
    3.53 +      } update_cartouches(replace_text, Path.explode(File.standard_path(file)))
    3.54      })
    3.55  }
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/Pure/Tools/update_comments.scala	Sun Jan 14 20:10:11 2018 +0100
     4.3 @@ -0,0 +1,63 @@
     4.4 +/*  Title:      Pure/Tools/update_comments.scala
     4.5 +    Author:     Makarius
     4.6 +
     4.7 +Update formal comments in outer syntax: \<comment> \<open>...\<close>
     4.8 +*/
     4.9 +
    4.10 +package isabelle
    4.11 +
    4.12 +
    4.13 +import scala.annotation.tailrec
    4.14 +
    4.15 +
    4.16 +object Update_Comments
    4.17 +{
    4.18 +  def update_comments(path: Path)
    4.19 +  {
    4.20 +    @tailrec def update(toks: List[Token], result: List[String]): String =
    4.21 +    {
    4.22 +      toks match {
    4.23 +        case tok :: rest if tok.source == "--" || tok.source == Symbol.comment =>
    4.24 +          rest.dropWhile(_.is_space) match {
    4.25 +            case tok1 :: rest1 if tok1.is_text =>
    4.26 +              val res = Symbol.comment + Symbol.space + Library.cartouche(tok1.content)
    4.27 +              update(rest1, res :: result)
    4.28 +            case _ => update(rest, tok.source :: result)
    4.29 +          }
    4.30 +        case tok :: rest => update(rest, tok.source :: result)
    4.31 +        case Nil => result.reverse.mkString
    4.32 +      }
    4.33 +    }
    4.34 +
    4.35 +    val text0 = File.read(path)
    4.36 +    val text1 = update(Token.explode(Keyword.Keywords.empty, text0), Nil)
    4.37 +
    4.38 +    if (text0 != text1) {
    4.39 +      Output.writeln("changing " + path)
    4.40 +      File.write_backup2(path, text1)
    4.41 +    }
    4.42 +  }
    4.43 +
    4.44 +
    4.45 +  /* Isabelle tool wrapper */
    4.46 +
    4.47 +  val isabelle_tool =
    4.48 +    Isabelle_Tool("update_comments", "update formal comments in outer syntax", args =>
    4.49 +    {
    4.50 +      val getopts = Getopts("""
    4.51 +Usage: isabelle update_comments [FILES|DIRS...]
    4.52 +
    4.53 +  Recursively find .thy files and update formal comments in outer syntax.
    4.54 +
    4.55 +  Old versions of files are preserved by appending "~~".
    4.56 +""")
    4.57 +
    4.58 +      val specs = getopts(args)
    4.59 +      if (specs.isEmpty) getopts.usage()
    4.60 +
    4.61 +      for {
    4.62 +        spec <- specs
    4.63 +        file <- File.find_files(Path.explode(spec).file, file => file.getName.endsWith(".thy"))
    4.64 +      } update_comments(Path.explode(File.standard_path(file)))
    4.65 +    })
    4.66 +}
     5.1 --- a/src/Pure/build-jars	Sun Jan 14 19:45:48 2018 +0100
     5.2 +++ b/src/Pure/build-jars	Sun Jan 14 20:10:11 2018 +0100
     5.3 @@ -148,6 +148,7 @@
     5.4    Tools/spell_checker.scala
     5.5    Tools/task_statistics.scala
     5.6    Tools/update_cartouches.scala
     5.7 +  Tools/update_comments.scala
     5.8    Tools/update_header.scala
     5.9    Tools/update_then.scala
    5.10    Tools/update_theorems.scala