support for multiple operations via options;
authorwenzelm
Sun Apr 23 16:18:31 2017 +0200 (2017-04-23)
changeset 65558479406635409
parent 65557 29c69a599743
child 65559 7ff7781913a4
support for multiple operations via options;
src/Pure/Tools/imports.scala
     1.1 --- a/src/Pure/Tools/imports.scala	Sun Apr 23 15:59:51 2017 +0200
     1.2 +++ b/src/Pure/Tools/imports.scala	Sun Apr 23 16:18:31 2017 +0200
     1.3 @@ -49,69 +49,6 @@
     1.4      }
     1.5    }
     1.6  
     1.7 -  def update_imports(
     1.8 -    options: Options,
     1.9 -    progress: Progress = No_Progress,
    1.10 -    selection: Sessions.Selection = Sessions.Selection.empty,
    1.11 -    dirs: List[Path] = Nil,
    1.12 -    select_dirs: List[Path] = Nil,
    1.13 -    verbose: Boolean = false): List[(JFile, Update)] =
    1.14 -  {
    1.15 -    val full_sessions = Sessions.load(options, dirs, select_dirs)
    1.16 -    val (selected, selected_sessions) = full_sessions.selection(selection)
    1.17 -
    1.18 -    val deps =
    1.19 -      Sessions.deps(selected_sessions, progress = progress, verbose = verbose,
    1.20 -        global_theories = full_sessions.global_theories)
    1.21 -
    1.22 -    selected.flatMap(session_name =>
    1.23 -    {
    1.24 -      val info = full_sessions(session_name)
    1.25 -      val session_base = deps(session_name)
    1.26 -      val session_resources = new Resources(session_base)
    1.27 -      val imports_resources = new Resources(session_base.get_imports)
    1.28 -
    1.29 -      val local_theories =
    1.30 -        (for {
    1.31 -          (_, name) <- session_base.known.theories_local.iterator
    1.32 -          if session_resources.theory_qualifier(name) == info.theory_qualifier
    1.33 -        } yield name).toSet
    1.34 -
    1.35 -      def standard_import(qualifier: String, dir: String, s: String): String =
    1.36 -      {
    1.37 -        val name = imports_resources.import_name(qualifier, dir, s)
    1.38 -        val file = Path.explode(name.node).file
    1.39 -        val s1 =
    1.40 -          imports_resources.session_base.known.get_file(file) match {
    1.41 -            case Some(name1) if session_resources.theory_qualifier(name1) != qualifier =>
    1.42 -              name1.theory
    1.43 -            case Some(name1) if Thy_Header.is_base_name(s) =>
    1.44 -              name1.theory_base_name
    1.45 -            case _ => s
    1.46 -          }
    1.47 -        val name2 = imports_resources.import_name(qualifier, dir, s1)
    1.48 -        if (name.node == name2.node) s1 else s
    1.49 -      }
    1.50 -
    1.51 -      val updates_root =
    1.52 -        for {
    1.53 -          (_, pos) <- info.theories.flatMap(_._2)
    1.54 -          upd <- update_name(Sessions.root_syntax.keywords, pos,
    1.55 -            standard_import(info.theory_qualifier, info.dir.implode, _))
    1.56 -        } yield upd
    1.57 -
    1.58 -      val updates_theories =
    1.59 -        for {
    1.60 -          (_, name) <- session_base.known.theories_local.toList
    1.61 -          (_, pos) <- session_resources.check_thy(name, Token.Pos.file(name.node)).imports
    1.62 -          upd <- update_name(session_base.syntax.keywords, pos,
    1.63 -            standard_import(session_resources.theory_qualifier(name), name.master_dir, _))
    1.64 -        } yield upd
    1.65 -
    1.66 -      updates_root ::: updates_theories
    1.67 -    })
    1.68 -  }
    1.69 -
    1.70    def apply_updates(updates: List[(JFile, Update)])
    1.71    {
    1.72      val file_updates = (Multi_Map.empty[JFile, Update] /: updates)(_ + _)
    1.73 @@ -144,6 +81,74 @@
    1.74      }
    1.75    }
    1.76  
    1.77 +  def imports(
    1.78 +    options: Options,
    1.79 +    operation_update: Boolean = false,
    1.80 +    progress: Progress = No_Progress,
    1.81 +    selection: Sessions.Selection = Sessions.Selection.empty,
    1.82 +    dirs: List[Path] = Nil,
    1.83 +    select_dirs: List[Path] = Nil,
    1.84 +    verbose: Boolean = false) =
    1.85 +  {
    1.86 +    val full_sessions = Sessions.load(options, dirs, select_dirs)
    1.87 +    val (selected, selected_sessions) = full_sessions.selection(selection)
    1.88 +
    1.89 +    val deps =
    1.90 +      Sessions.deps(selected_sessions, progress = progress, verbose = verbose,
    1.91 +        global_theories = full_sessions.global_theories)
    1.92 +
    1.93 +    if (operation_update) {
    1.94 +      val updates =
    1.95 +        selected.flatMap(session_name =>
    1.96 +        {
    1.97 +          val info = full_sessions(session_name)
    1.98 +          val session_base = deps(session_name)
    1.99 +          val session_resources = new Resources(session_base)
   1.100 +          val imports_resources = new Resources(session_base.get_imports)
   1.101 +
   1.102 +          val local_theories =
   1.103 +            (for {
   1.104 +              (_, name) <- session_base.known.theories_local.iterator
   1.105 +              if session_resources.theory_qualifier(name) == info.theory_qualifier
   1.106 +            } yield name).toSet
   1.107 +
   1.108 +          def standard_import(qualifier: String, dir: String, s: String): String =
   1.109 +          {
   1.110 +            val name = imports_resources.import_name(qualifier, dir, s)
   1.111 +            val file = Path.explode(name.node).file
   1.112 +            val s1 =
   1.113 +              imports_resources.session_base.known.get_file(file) match {
   1.114 +                case Some(name1) if session_resources.theory_qualifier(name1) != qualifier =>
   1.115 +                  name1.theory
   1.116 +                case Some(name1) if Thy_Header.is_base_name(s) =>
   1.117 +                  name1.theory_base_name
   1.118 +                case _ => s
   1.119 +              }
   1.120 +            val name2 = imports_resources.import_name(qualifier, dir, s1)
   1.121 +            if (name.node == name2.node) s1 else s
   1.122 +          }
   1.123 +
   1.124 +          val updates_root =
   1.125 +            for {
   1.126 +              (_, pos) <- info.theories.flatMap(_._2)
   1.127 +              upd <- update_name(Sessions.root_syntax.keywords, pos,
   1.128 +                standard_import(info.theory_qualifier, info.dir.implode, _))
   1.129 +            } yield upd
   1.130 +
   1.131 +          val updates_theories =
   1.132 +            for {
   1.133 +              (_, name) <- session_base.known.theories_local.toList
   1.134 +              (_, pos) <- session_resources.check_thy(name, Token.Pos.file(name.node)).imports
   1.135 +              upd <- update_name(session_base.syntax.keywords, pos,
   1.136 +                standard_import(session_resources.theory_qualifier(name), name.master_dir, _))
   1.137 +            } yield upd
   1.138 +
   1.139 +          updates_root ::: updates_theories
   1.140 +        })
   1.141 +      apply_updates(updates)
   1.142 +    }
   1.143 +  }
   1.144 +
   1.145  
   1.146    /* Isabelle tool wrapper */
   1.147  
   1.148 @@ -152,6 +157,7 @@
   1.149      {
   1.150        var select_dirs: List[Path] = Nil
   1.151        var requirements = false
   1.152 +      var operation_update = false
   1.153        var exclude_session_groups: List[String] = Nil
   1.154        var all_sessions = false
   1.155        var dirs: List[Path] = Nil
   1.156 @@ -166,6 +172,7 @@
   1.157    Options are:
   1.158      -D DIR       include session directory and select its sessions
   1.159      -R           operate on requirements of selected sessions
   1.160 +    -U           operation: update theory imports to use session qualifiers
   1.161      -X NAME      exclude sessions from group NAME and all descendants
   1.162      -a           select all sessions
   1.163      -d DIR       include session directory
   1.164 @@ -174,12 +181,12 @@
   1.165      -v           verbose
   1.166      -x NAME      exclude session NAME and all descendants
   1.167  
   1.168 -  Maintain theory imports wrt. session structure.
   1.169 -
   1.170 -  Old versions of files are preserved by appending "~~".
   1.171 +  Maintain theory imports wrt. session structure. At least one operation
   1.172 +  needs to be specified (see option -U).
   1.173  """,
   1.174        "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
   1.175        "R" -> (_ => requirements = true),
   1.176 +      "U" -> (_ => operation_update = true),
   1.177        "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
   1.178        "a" -> (_ => all_sessions = true),
   1.179        "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
   1.180 @@ -189,7 +196,7 @@
   1.181        "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg)))
   1.182  
   1.183        val sessions = getopts(args)
   1.184 -      if (args.isEmpty) getopts.usage()
   1.185 +      if (args.isEmpty || !operation_update) getopts.usage()
   1.186  
   1.187        val selection =
   1.188          Sessions.Selection(requirements, all_sessions, exclude_session_groups,
   1.189 @@ -197,10 +204,7 @@
   1.190  
   1.191        val progress = new Console_Progress(verbose = verbose)
   1.192  
   1.193 -      val updates =
   1.194 -        update_imports(options, progress = progress, selection = selection,
   1.195 -          dirs = dirs, select_dirs = select_dirs, verbose = verbose)
   1.196 -
   1.197 -      apply_updates(updates)
   1.198 +      imports(options, operation_update = operation_update, progress = progress,
   1.199 +        selection = selection, dirs = dirs, select_dirs = select_dirs, verbose = verbose)
   1.200      })
   1.201  }