clarified tool name -- more official status;
authorwenzelm
Sun Apr 23 15:59:51 2017 +0200 (2017-04-23)
changeset 6555729c69a599743
parent 65554 a04afc400156
child 65558 479406635409
clarified tool name -- more official status;
NEWS
src/Pure/System/isabelle_tool.scala
src/Pure/Tools/imports.scala
src/Pure/Tools/update_imports.scala
src/Pure/build-jars
     1.1 --- a/NEWS	Sun Apr 23 14:27:22 2017 +0200
     1.2 +++ b/NEWS	Sun Apr 23 15:59:51 2017 +0200
     1.3 @@ -201,6 +201,9 @@
     1.4  a negative value means the current state in the ML heap image remains
     1.5  unchanged.
     1.6  
     1.7 +* Command-line tool "isabelle imports" helps to maintain theory imports
     1.8 +wrt. session structure.
     1.9 +
    1.10  
    1.11  
    1.12  New in Isabelle2016-1 (December 2016)
     2.1 --- a/src/Pure/System/isabelle_tool.scala	Sun Apr 23 14:27:22 2017 +0200
     2.2 +++ b/src/Pure/System/isabelle_tool.scala	Sun Apr 23 15:59:51 2017 +0200
     2.3 @@ -108,6 +108,7 @@
     2.4        Build_Stats.isabelle_tool,
     2.5        Check_Sources.isabelle_tool,
     2.6        Doc.isabelle_tool,
     2.7 +      Imports.isabelle_tool,
     2.8        ML_Process.isabelle_tool,
     2.9        NEWS.isabelle_tool,
    2.10        Options.isabelle_tool,
    2.11 @@ -115,7 +116,6 @@
    2.12        Remote_DMG.isabelle_tool,
    2.13        Update_Cartouches.isabelle_tool,
    2.14        Update_Header.isabelle_tool,
    2.15 -      Update_Imports.isabelle_tool,
    2.16        Update_Then.isabelle_tool,
    2.17        Update_Theorems.isabelle_tool,
    2.18        isabelle.vscode.Build_VSCode.isabelle_tool,
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/Pure/Tools/imports.scala	Sun Apr 23 15:59:51 2017 +0200
     3.3 @@ -0,0 +1,206 @@
     3.4 +/*  Title:      Pure/Tools/imports.scala
     3.5 +    Author:     Makarius
     3.6 +
     3.7 +Maintain theory imports wrt. session structure.
     3.8 +*/
     3.9 +
    3.10 +package isabelle
    3.11 +
    3.12 +
    3.13 +import java.io.{File => JFile}
    3.14 +
    3.15 +
    3.16 +object Imports
    3.17 +{
    3.18 +  /* update imports */
    3.19 +
    3.20 +  sealed case class Update(range: Text.Range, old_text: String, new_text: String)
    3.21 +  {
    3.22 +    def edits: List[Text.Edit] =
    3.23 +      Text.Edit.replace(range.start, old_text, new_text)
    3.24 +
    3.25 +    override def toString: String =
    3.26 +      range.toString + ": " + old_text + " -> " + new_text
    3.27 +  }
    3.28 +
    3.29 +  def update_name(keywords: Keyword.Keywords, pos: Position.T, update: String => String)
    3.30 +    : Option[(JFile, Update)] =
    3.31 +  {
    3.32 +    val file =
    3.33 +      pos match {
    3.34 +        case Position.File(file) => Path.explode(file).file.getCanonicalFile
    3.35 +        case _ => error("Missing file in position" + Position.here(pos))
    3.36 +      }
    3.37 +
    3.38 +    val text = File.read(file)
    3.39 +
    3.40 +    val range =
    3.41 +      pos match {
    3.42 +        case Position.Range(symbol_range) => Symbol.Text_Chunk(text).decode(symbol_range)
    3.43 +        case _ => error("Missing range in position" + Position.here(pos))
    3.44 +      }
    3.45 +
    3.46 +    Token.read_name(keywords, range.substring(text)) match {
    3.47 +      case Some(tok) =>
    3.48 +        val s1 = tok.source
    3.49 +        val s2 = Token.quote_name(keywords, update(tok.content))
    3.50 +        if (s1 == s2) None else Some((file, Update(range, s1, s2)))
    3.51 +      case None => error("Name token expected" + Position.here(pos))
    3.52 +    }
    3.53 +  }
    3.54 +
    3.55 +  def update_imports(
    3.56 +    options: Options,
    3.57 +    progress: Progress = No_Progress,
    3.58 +    selection: Sessions.Selection = Sessions.Selection.empty,
    3.59 +    dirs: List[Path] = Nil,
    3.60 +    select_dirs: List[Path] = Nil,
    3.61 +    verbose: Boolean = false): List[(JFile, Update)] =
    3.62 +  {
    3.63 +    val full_sessions = Sessions.load(options, dirs, select_dirs)
    3.64 +    val (selected, selected_sessions) = full_sessions.selection(selection)
    3.65 +
    3.66 +    val deps =
    3.67 +      Sessions.deps(selected_sessions, progress = progress, verbose = verbose,
    3.68 +        global_theories = full_sessions.global_theories)
    3.69 +
    3.70 +    selected.flatMap(session_name =>
    3.71 +    {
    3.72 +      val info = full_sessions(session_name)
    3.73 +      val session_base = deps(session_name)
    3.74 +      val session_resources = new Resources(session_base)
    3.75 +      val imports_resources = new Resources(session_base.get_imports)
    3.76 +
    3.77 +      val local_theories =
    3.78 +        (for {
    3.79 +          (_, name) <- session_base.known.theories_local.iterator
    3.80 +          if session_resources.theory_qualifier(name) == info.theory_qualifier
    3.81 +        } yield name).toSet
    3.82 +
    3.83 +      def standard_import(qualifier: String, dir: String, s: String): String =
    3.84 +      {
    3.85 +        val name = imports_resources.import_name(qualifier, dir, s)
    3.86 +        val file = Path.explode(name.node).file
    3.87 +        val s1 =
    3.88 +          imports_resources.session_base.known.get_file(file) match {
    3.89 +            case Some(name1) if session_resources.theory_qualifier(name1) != qualifier =>
    3.90 +              name1.theory
    3.91 +            case Some(name1) if Thy_Header.is_base_name(s) =>
    3.92 +              name1.theory_base_name
    3.93 +            case _ => s
    3.94 +          }
    3.95 +        val name2 = imports_resources.import_name(qualifier, dir, s1)
    3.96 +        if (name.node == name2.node) s1 else s
    3.97 +      }
    3.98 +
    3.99 +      val updates_root =
   3.100 +        for {
   3.101 +          (_, pos) <- info.theories.flatMap(_._2)
   3.102 +          upd <- update_name(Sessions.root_syntax.keywords, pos,
   3.103 +            standard_import(info.theory_qualifier, info.dir.implode, _))
   3.104 +        } yield upd
   3.105 +
   3.106 +      val updates_theories =
   3.107 +        for {
   3.108 +          (_, name) <- session_base.known.theories_local.toList
   3.109 +          (_, pos) <- session_resources.check_thy(name, Token.Pos.file(name.node)).imports
   3.110 +          upd <- update_name(session_base.syntax.keywords, pos,
   3.111 +            standard_import(session_resources.theory_qualifier(name), name.master_dir, _))
   3.112 +        } yield upd
   3.113 +
   3.114 +      updates_root ::: updates_theories
   3.115 +    })
   3.116 +  }
   3.117 +
   3.118 +  def apply_updates(updates: List[(JFile, Update)])
   3.119 +  {
   3.120 +    val file_updates = (Multi_Map.empty[JFile, Update] /: updates)(_ + _)
   3.121 +    val conflicts =
   3.122 +      file_updates.iterator_list.flatMap({ case (file, upds) =>
   3.123 +        Library.duplicates(upds.sortBy(_.range.start),
   3.124 +          (x: Update, y: Update) => x.range overlaps y.range) match
   3.125 +        {
   3.126 +          case Nil => None
   3.127 +          case bad => Some((file, bad))
   3.128 +        }
   3.129 +      })
   3.130 +    if (conflicts.nonEmpty)
   3.131 +      error(cat_lines(
   3.132 +        conflicts.map({ case (file, bad) =>
   3.133 +          "Conflicting updates for file " + file + bad.mkString("\n  ", "\n  ", "") })))
   3.134 +
   3.135 +    for ((file, upds) <- file_updates.iterator_list) {
   3.136 +      val edits =
   3.137 +        upds.sortBy(upd => - upd.range.start).flatMap(upd =>
   3.138 +          Text.Edit.replace(upd.range.start, upd.old_text, upd.new_text))
   3.139 +      val new_text =
   3.140 +        (File.read(file) /: edits)({ case (text, edit) =>
   3.141 +          edit.edit(text, 0) match {
   3.142 +            case (None, text1) => text1
   3.143 +            case (Some(_), _) => error("Failed to apply edit " + edit + " to file " + file)
   3.144 +          }
   3.145 +        })
   3.146 +      File.write_backup2(Path.explode(File.standard_path(file)), new_text)
   3.147 +    }
   3.148 +  }
   3.149 +
   3.150 +
   3.151 +  /* Isabelle tool wrapper */
   3.152 +
   3.153 +  val isabelle_tool =
   3.154 +    Isabelle_Tool("imports", "maintain theory imports wrt. session structure", args =>
   3.155 +    {
   3.156 +      var select_dirs: List[Path] = Nil
   3.157 +      var requirements = false
   3.158 +      var exclude_session_groups: List[String] = Nil
   3.159 +      var all_sessions = false
   3.160 +      var dirs: List[Path] = Nil
   3.161 +      var session_groups: List[String] = Nil
   3.162 +      var options = Options.init()
   3.163 +      var verbose = false
   3.164 +      var exclude_sessions: List[String] = Nil
   3.165 +
   3.166 +      val getopts = Getopts("""
   3.167 +Usage: isabelle imports [OPTIONS] [SESSIONS ...]
   3.168 +
   3.169 +  Options are:
   3.170 +    -D DIR       include session directory and select its sessions
   3.171 +    -R           operate on requirements of selected sessions
   3.172 +    -X NAME      exclude sessions from group NAME and all descendants
   3.173 +    -a           select all sessions
   3.174 +    -d DIR       include session directory
   3.175 +    -g NAME      select session group NAME
   3.176 +    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
   3.177 +    -v           verbose
   3.178 +    -x NAME      exclude session NAME and all descendants
   3.179 +
   3.180 +  Maintain theory imports wrt. session structure.
   3.181 +
   3.182 +  Old versions of files are preserved by appending "~~".
   3.183 +""",
   3.184 +      "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
   3.185 +      "R" -> (_ => requirements = true),
   3.186 +      "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
   3.187 +      "a" -> (_ => all_sessions = true),
   3.188 +      "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
   3.189 +      "g:" -> (arg => session_groups = session_groups ::: List(arg)),
   3.190 +      "o:" -> (arg => options = options + arg),
   3.191 +      "v" -> (_ => verbose = true),
   3.192 +      "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg)))
   3.193 +
   3.194 +      val sessions = getopts(args)
   3.195 +      if (args.isEmpty) getopts.usage()
   3.196 +
   3.197 +      val selection =
   3.198 +        Sessions.Selection(requirements, all_sessions, exclude_session_groups,
   3.199 +          exclude_sessions, session_groups, sessions)
   3.200 +
   3.201 +      val progress = new Console_Progress(verbose = verbose)
   3.202 +
   3.203 +      val updates =
   3.204 +        update_imports(options, progress = progress, selection = selection,
   3.205 +          dirs = dirs, select_dirs = select_dirs, verbose = verbose)
   3.206 +
   3.207 +      apply_updates(updates)
   3.208 +    })
   3.209 +}
     4.1 --- a/src/Pure/Tools/update_imports.scala	Sun Apr 23 14:27:22 2017 +0200
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,206 +0,0 @@
     4.4 -/*  Title:      Pure/Tools/update_imports.scala
     4.5 -    Author:     Makarius
     4.6 -
     4.7 -Update theory imports to use session qualifiers.
     4.8 -*/
     4.9 -
    4.10 -package isabelle
    4.11 -
    4.12 -
    4.13 -import java.io.{File => JFile}
    4.14 -
    4.15 -
    4.16 -object Update_Imports
    4.17 -{
    4.18 -  /* update imports */
    4.19 -
    4.20 -  sealed case class Update(range: Text.Range, old_text: String, new_text: String)
    4.21 -  {
    4.22 -    def edits: List[Text.Edit] =
    4.23 -      Text.Edit.replace(range.start, old_text, new_text)
    4.24 -
    4.25 -    override def toString: String =
    4.26 -      range.toString + ": " + old_text + " -> " + new_text
    4.27 -  }
    4.28 -
    4.29 -  def update_name(keywords: Keyword.Keywords, pos: Position.T, update: String => String)
    4.30 -    : Option[(JFile, Update)] =
    4.31 -  {
    4.32 -    val file =
    4.33 -      pos match {
    4.34 -        case Position.File(file) => Path.explode(file).file.getCanonicalFile
    4.35 -        case _ => error("Missing file in position" + Position.here(pos))
    4.36 -      }
    4.37 -
    4.38 -    val text = File.read(file)
    4.39 -
    4.40 -    val range =
    4.41 -      pos match {
    4.42 -        case Position.Range(symbol_range) => Symbol.Text_Chunk(text).decode(symbol_range)
    4.43 -        case _ => error("Missing range in position" + Position.here(pos))
    4.44 -      }
    4.45 -
    4.46 -    Token.read_name(keywords, range.substring(text)) match {
    4.47 -      case Some(tok) =>
    4.48 -        val s1 = tok.source
    4.49 -        val s2 = Token.quote_name(keywords, update(tok.content))
    4.50 -        if (s1 == s2) None else Some((file, Update(range, s1, s2)))
    4.51 -      case None => error("Name token expected" + Position.here(pos))
    4.52 -    }
    4.53 -  }
    4.54 -
    4.55 -  def update_imports(
    4.56 -    options: Options,
    4.57 -    progress: Progress = No_Progress,
    4.58 -    selection: Sessions.Selection = Sessions.Selection.empty,
    4.59 -    dirs: List[Path] = Nil,
    4.60 -    select_dirs: List[Path] = Nil,
    4.61 -    verbose: Boolean = false): List[(JFile, Update)] =
    4.62 -  {
    4.63 -    val full_sessions = Sessions.load(options, dirs, select_dirs)
    4.64 -    val (selected, selected_sessions) = full_sessions.selection(selection)
    4.65 -
    4.66 -    val deps =
    4.67 -      Sessions.deps(selected_sessions, progress = progress, verbose = verbose,
    4.68 -        global_theories = full_sessions.global_theories)
    4.69 -
    4.70 -    selected.flatMap(session_name =>
    4.71 -    {
    4.72 -      val info = full_sessions(session_name)
    4.73 -      val session_base = deps(session_name)
    4.74 -      val session_resources = new Resources(session_base)
    4.75 -      val imports_resources = new Resources(session_base.get_imports)
    4.76 -
    4.77 -      val local_theories =
    4.78 -        (for {
    4.79 -          (_, name) <- session_base.known.theories_local.iterator
    4.80 -          if session_resources.theory_qualifier(name) == info.theory_qualifier
    4.81 -        } yield name).toSet
    4.82 -
    4.83 -      def standard_import(qualifier: String, dir: String, s: String): String =
    4.84 -      {
    4.85 -        val name = imports_resources.import_name(qualifier, dir, s)
    4.86 -        val file = Path.explode(name.node).file
    4.87 -        val s1 =
    4.88 -          imports_resources.session_base.known.get_file(file) match {
    4.89 -            case Some(name1) if session_resources.theory_qualifier(name1) != qualifier =>
    4.90 -              name1.theory
    4.91 -            case Some(name1) if Thy_Header.is_base_name(s) =>
    4.92 -              name1.theory_base_name
    4.93 -            case _ => s
    4.94 -          }
    4.95 -        val name2 = imports_resources.import_name(qualifier, dir, s1)
    4.96 -        if (name.node == name2.node) s1 else s
    4.97 -      }
    4.98 -
    4.99 -      val updates_root =
   4.100 -        for {
   4.101 -          (_, pos) <- info.theories.flatMap(_._2)
   4.102 -          upd <- update_name(Sessions.root_syntax.keywords, pos,
   4.103 -            standard_import(info.theory_qualifier, info.dir.implode, _))
   4.104 -        } yield upd
   4.105 -
   4.106 -      val updates_theories =
   4.107 -        for {
   4.108 -          (_, name) <- session_base.known.theories_local.toList
   4.109 -          (_, pos) <- session_resources.check_thy(name, Token.Pos.file(name.node)).imports
   4.110 -          upd <- update_name(session_base.syntax.keywords, pos,
   4.111 -            standard_import(session_resources.theory_qualifier(name), name.master_dir, _))
   4.112 -        } yield upd
   4.113 -
   4.114 -      updates_root ::: updates_theories
   4.115 -    })
   4.116 -  }
   4.117 -
   4.118 -  def apply_updates(updates: List[(JFile, Update)])
   4.119 -  {
   4.120 -    val file_updates = (Multi_Map.empty[JFile, Update] /: updates)(_ + _)
   4.121 -    val conflicts =
   4.122 -      file_updates.iterator_list.flatMap({ case (file, upds) =>
   4.123 -        Library.duplicates(upds.sortBy(_.range.start),
   4.124 -          (x: Update, y: Update) => x.range overlaps y.range) match
   4.125 -        {
   4.126 -          case Nil => None
   4.127 -          case bad => Some((file, bad))
   4.128 -        }
   4.129 -      })
   4.130 -    if (conflicts.nonEmpty)
   4.131 -      error(cat_lines(
   4.132 -        conflicts.map({ case (file, bad) =>
   4.133 -          "Conflicting updates for file " + file + bad.mkString("\n  ", "\n  ", "") })))
   4.134 -
   4.135 -    for ((file, upds) <- file_updates.iterator_list) {
   4.136 -      val edits =
   4.137 -        upds.sortBy(upd => - upd.range.start).flatMap(upd =>
   4.138 -          Text.Edit.replace(upd.range.start, upd.old_text, upd.new_text))
   4.139 -      val new_text =
   4.140 -        (File.read(file) /: edits)({ case (text, edit) =>
   4.141 -          edit.edit(text, 0) match {
   4.142 -            case (None, text1) => text1
   4.143 -            case (Some(_), _) => error("Failed to apply edit " + edit + " to file " + file)
   4.144 -          }
   4.145 -        })
   4.146 -      File.write_backup2(Path.explode(File.standard_path(file)), new_text)
   4.147 -    }
   4.148 -  }
   4.149 -
   4.150 -
   4.151 -  /* Isabelle tool wrapper */
   4.152 -
   4.153 -  val isabelle_tool =
   4.154 -    Isabelle_Tool("update_imports", "update theory imports to use session qualifiers", args =>
   4.155 -    {
   4.156 -      var select_dirs: List[Path] = Nil
   4.157 -      var requirements = false
   4.158 -      var exclude_session_groups: List[String] = Nil
   4.159 -      var all_sessions = false
   4.160 -      var dirs: List[Path] = Nil
   4.161 -      var session_groups: List[String] = Nil
   4.162 -      var options = Options.init()
   4.163 -      var verbose = false
   4.164 -      var exclude_sessions: List[String] = Nil
   4.165 -
   4.166 -      val getopts = Getopts("""
   4.167 -Usage: isabelle update_imports [OPTIONS] [SESSIONS ...]
   4.168 -
   4.169 -  Options are:
   4.170 -    -D DIR       include session directory and select its sessions
   4.171 -    -R           operate on requirements of selected sessions
   4.172 -    -X NAME      exclude sessions from group NAME and all descendants
   4.173 -    -a           select all sessions
   4.174 -    -d DIR       include session directory
   4.175 -    -g NAME      select session group NAME
   4.176 -    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
   4.177 -    -v           verbose
   4.178 -    -x NAME      exclude session NAME and all descendants
   4.179 -
   4.180 -  Update theory imports to use session qualifiers.
   4.181 -
   4.182 -  Old versions of files are preserved by appending "~~".
   4.183 -""",
   4.184 -      "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
   4.185 -      "R" -> (_ => requirements = true),
   4.186 -      "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
   4.187 -      "a" -> (_ => all_sessions = true),
   4.188 -      "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
   4.189 -      "g:" -> (arg => session_groups = session_groups ::: List(arg)),
   4.190 -      "o:" -> (arg => options = options + arg),
   4.191 -      "v" -> (_ => verbose = true),
   4.192 -      "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg)))
   4.193 -
   4.194 -      val sessions = getopts(args)
   4.195 -      if (args.isEmpty) getopts.usage()
   4.196 -
   4.197 -      val selection =
   4.198 -        Sessions.Selection(requirements, all_sessions, exclude_session_groups,
   4.199 -          exclude_sessions, session_groups, sessions)
   4.200 -
   4.201 -      val progress = new Console_Progress(verbose = verbose)
   4.202 -
   4.203 -      val updates =
   4.204 -        update_imports(options, progress = progress, selection = selection,
   4.205 -          dirs = dirs, select_dirs = select_dirs, verbose = verbose)
   4.206 -
   4.207 -      apply_updates(updates)
   4.208 -    })
   4.209 -}
     5.1 --- a/src/Pure/build-jars	Sun Apr 23 14:27:22 2017 +0200
     5.2 +++ b/src/Pure/build-jars	Sun Apr 23 15:59:51 2017 +0200
     5.3 @@ -135,6 +135,7 @@
     5.4    Tools/check_keywords.scala
     5.5    Tools/debugger.scala
     5.6    Tools/doc.scala
     5.7 +  Tools/imports.scala
     5.8    Tools/main.scala
     5.9    Tools/print_operation.scala
    5.10    Tools/profiling_report.scala
    5.11 @@ -143,7 +144,6 @@
    5.12    Tools/task_statistics.scala
    5.13    Tools/update_cartouches.scala
    5.14    Tools/update_header.scala
    5.15 -  Tools/update_imports.scala
    5.16    Tools/update_then.scala
    5.17    Tools/update_theorems.scala
    5.18    library.scala