read Pure file dependencies directly from ROOT.ML;
authorwenzelm
Tue Apr 05 15:27:11 2016 +0200 (2016-04-05)
changeset 62866d20262cd20e8
parent 62865 cf03cb9578d4
child 62867 cce0570d1bfa
read Pure file dependencies directly from ROOT.ML;
src/Pure/ML/ml_root.scala
src/Pure/ROOT
src/Pure/Tools/build.scala
src/Pure/build-jars
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/ML/ml_root.scala	Tue Apr 05 15:27:11 2016 +0200
     1.3 @@ -0,0 +1,54 @@
     1.4 +/*  Title:      Pure/ML/ml_root.scala
     1.5 +    Author:     Makarius
     1.6 +
     1.7 +Support for ML project ROOT file, with imitation of ML "use" commands.
     1.8 +*/
     1.9 +
    1.10 +package isabelle
    1.11 +
    1.12 +
    1.13 +object ML_Root
    1.14 +{
    1.15 +  /* parser */
    1.16 +
    1.17 +  val ROOT_ML = Path.explode("ROOT.ML")
    1.18 +
    1.19 +  val USE = "use"
    1.20 +  val USE_DEBUG = "use_debug"
    1.21 +  val USE_NO_DEBUG = "use_no_debug"
    1.22 +  val USE_THY = "use_thy"
    1.23 +
    1.24 +  lazy val syntax =
    1.25 +    Outer_Syntax.init() + ";" +
    1.26 +      (USE, Some((Keyword.THY_LOAD, Nil)), None) +
    1.27 +      (USE_DEBUG, Some((Keyword.THY_LOAD, Nil)), None) +
    1.28 +      (USE_NO_DEBUG, Some((Keyword.THY_LOAD, Nil)), None) +
    1.29 +      (USE_THY, Some((Keyword.THY_LOAD, Nil)), None)
    1.30 +
    1.31 +  private object Parser extends Parse.Parser
    1.32 +  {
    1.33 +    val entry: Parser[(String, String)] =
    1.34 +      (command(USE) | command(USE_DEBUG) | command(USE_NO_DEBUG) | command(USE_THY)) ~!
    1.35 +        (string ~ $$$(";")) ^^ { case a ~ (b ~ _) => (a, b) }
    1.36 +
    1.37 +    def parse(in: Token.Reader): ParseResult[List[(String, String)]] =
    1.38 +      parse_all(rep(entry), in)
    1.39 +  }
    1.40 +
    1.41 +  def read(dir: Path): List[(String, Path)] =
    1.42 +  {
    1.43 +    val root = dir + ROOT_ML
    1.44 +
    1.45 +    val toks = Token.explode(syntax.keywords, File.read(root))
    1.46 +    val start = Token.Pos.file(root.implode)
    1.47 +
    1.48 +    Parser.parse(Token.reader(toks, start)) match {
    1.49 +      case Parser.Success(entries, _) =>
    1.50 +        for ((a, b) <- entries) yield {
    1.51 +          val path = dir + Path.explode(b)
    1.52 +          (a, if (a == USE_THY) Resources.thy_path(path) else path)
    1.53 +        }
    1.54 +      case bad => error(bad.toString)
    1.55 +    }
    1.56 +  }
    1.57 +}
     2.1 --- a/src/Pure/ROOT	Tue Apr 05 14:59:00 2016 +0200
     2.2 +++ b/src/Pure/ROOT	Tue Apr 05 15:27:11 2016 +0200
     2.3 @@ -2,240 +2,4 @@
     2.4  
     2.5  session Pure =
     2.6    global_theories Pure
     2.7 -  files
     2.8 -    "Concurrent/cache.ML"
     2.9 -    "Concurrent/counter.ML"
    2.10 -    "Concurrent/event_timer.ML"
    2.11 -    "Concurrent/future.ML"
    2.12 -    "Concurrent/lazy.ML"
    2.13 -    "Concurrent/mailbox.ML"
    2.14 -    "Concurrent/multithreading.ML"
    2.15 -    "Concurrent/par_exn.ML"
    2.16 -    "Concurrent/par_list.ML"
    2.17 -    "Concurrent/single_assignment.ML"
    2.18 -    "Concurrent/standard_thread.ML"
    2.19 -    "Concurrent/synchronized.ML"
    2.20 -    "Concurrent/task_queue.ML"
    2.21 -    "Concurrent/timeout.ML"
    2.22 -    "Concurrent/unsynchronized.ML"
    2.23 -    "General/alist.ML"
    2.24 -    "General/antiquote.ML"
    2.25 -    "General/balanced_tree.ML"
    2.26 -    "General/basics.ML"
    2.27 -    "General/binding.ML"
    2.28 -    "General/buffer.ML"
    2.29 -    "General/change_table.ML"
    2.30 -    "General/completion.ML"
    2.31 -    "General/exn.ML"
    2.32 -    "General/file.ML"
    2.33 -    "General/graph.ML"
    2.34 -    "General/graph_display.ML"
    2.35 -    "General/heap.ML"
    2.36 -    "General/input.ML"
    2.37 -    "General/integer.ML"
    2.38 -    "General/linear_set.ML"
    2.39 -    "General/long_name.ML"
    2.40 -    "General/name_space.ML"
    2.41 -    "General/ord_list.ML"
    2.42 -    "General/output.ML"
    2.43 -    "General/path.ML"
    2.44 -    "General/position.ML"
    2.45 -    "General/pretty.ML"
    2.46 -    "General/print_mode.ML"
    2.47 -    "General/properties.ML"
    2.48 -    "General/queue.ML"
    2.49 -    "General/random.ML"
    2.50 -    "General/same.ML"
    2.51 -    "General/scan.ML"
    2.52 -    "General/seq.ML"
    2.53 -    "General/sha1.ML"
    2.54 -    "General/socket_io.ML"
    2.55 -    "General/source.ML"
    2.56 -    "General/stack.ML"
    2.57 -    "General/symbol.ML"
    2.58 -    "General/symbol_pos.ML"
    2.59 -    "General/table.ML"
    2.60 -    "General/timing.ML"
    2.61 -    "General/url.ML"
    2.62 -    "Isar/args.ML"
    2.63 -    "Isar/attrib.ML"
    2.64 -    "Isar/auto_bind.ML"
    2.65 -    "Isar/bundle.ML"
    2.66 -    "Isar/calculation.ML"
    2.67 -    "Isar/class.ML"
    2.68 -    "Isar/class_declaration.ML"
    2.69 -    "Isar/code.ML"
    2.70 -    "Isar/context_rules.ML"
    2.71 -    "Isar/element.ML"
    2.72 -    "Isar/experiment.ML"
    2.73 -    "Isar/expression.ML"
    2.74 -    "Isar/generic_target.ML"
    2.75 -    "Isar/interpretation.ML"
    2.76 -    "Isar/isar_cmd.ML"
    2.77 -    "Isar/keyword.ML"
    2.78 -    "Isar/local_defs.ML"
    2.79 -    "Isar/local_theory.ML"
    2.80 -    "Isar/locale.ML"
    2.81 -    "Isar/method.ML"
    2.82 -    "Isar/named_target.ML"
    2.83 -    "Isar/object_logic.ML"
    2.84 -    "Isar/obtain.ML"
    2.85 -    "Isar/outer_syntax.ML"
    2.86 -    "Isar/overloading.ML"
    2.87 -    "Isar/parse.ML"
    2.88 -    "Isar/parse_spec.ML"
    2.89 -    "Isar/proof.ML"
    2.90 -    "Isar/proof_context.ML"
    2.91 -    "Isar/proof_display.ML"
    2.92 -    "Isar/proof_node.ML"
    2.93 -    "Isar/rule_cases.ML"
    2.94 -    "Isar/runtime.ML"
    2.95 -    "Isar/spec_rules.ML"
    2.96 -    "Isar/specification.ML"
    2.97 -    "Isar/subgoal.ML"
    2.98 -    "Isar/token.ML"
    2.99 -    "Isar/toplevel.ML"
   2.100 -    "Isar/typedecl.ML"
   2.101 -    "ML/exn_debugger.ML"
   2.102 -    "ML/exn_properties.ML"
   2.103 -    "ML/ml_antiquotation.ML"
   2.104 -    "ML/ml_antiquotations.ML"
   2.105 -    "ML/ml_compiler.ML"
   2.106 -    "ML/ml_compiler0.ML"
   2.107 -    "ML/ml_compiler1.ML"
   2.108 -    "ML/ml_compiler2.ML"
   2.109 -    "ML/ml_context.ML"
   2.110 -    "ML/ml_debugger.ML"
   2.111 -    "ML/ml_env.ML"
   2.112 -    "ML/ml_file.ML"
   2.113 -    "ML/ml_heap.ML"
   2.114 -    "ML/ml_lex.ML"
   2.115 -    "ML/ml_name_space.ML"
   2.116 -    "ML/ml_options.ML"
   2.117 -    "ML/ml_pervasive_final.ML"
   2.118 -    "ML/ml_pervasive_initial.ML"
   2.119 -    "ML/ml_pp.ML"
   2.120 -    "ML/ml_pretty.ML"
   2.121 -    "ML/ml_profiling.ML"
   2.122 -    "ML/ml_statistics.ML"
   2.123 -    "ML/ml_syntax.ML"
   2.124 -    "ML/ml_system.ML"
   2.125 -    "ML/ml_thms.ML"
   2.126 -    "PIDE/active.ML"
   2.127 -    "PIDE/command.ML"
   2.128 -    "PIDE/command_span.ML"
   2.129 -    "PIDE/document.ML"
   2.130 -    "PIDE/document_id.ML"
   2.131 -    "PIDE/execution.ML"
   2.132 -    "PIDE/markup.ML"
   2.133 -    "PIDE/protocol.ML"
   2.134 -    "PIDE/protocol_message.ML"
   2.135 -    "PIDE/query_operation.ML"
   2.136 -    "PIDE/resources.ML"
   2.137 -    "PIDE/session.ML"
   2.138 -    "PIDE/xml.ML"
   2.139 -    "PIDE/yxml.ML"
   2.140 -    "Proof/extraction.ML"
   2.141 -    "Proof/proof_checker.ML"
   2.142 -    "Proof/proof_rewrite_rules.ML"
   2.143 -    "Proof/proof_syntax.ML"
   2.144 -    "Proof/reconstruct.ML"
   2.145 -    "ROOT.ML"
   2.146 -    "Syntax/ast.ML"
   2.147 -    "Syntax/lexicon.ML"
   2.148 -    "Syntax/local_syntax.ML"
   2.149 -    "Syntax/mixfix.ML"
   2.150 -    "Syntax/parser.ML"
   2.151 -    "Syntax/printer.ML"
   2.152 -    "Syntax/simple_syntax.ML"
   2.153 -    "Syntax/syntax.ML"
   2.154 -    "Syntax/syntax_ext.ML"
   2.155 -    "Syntax/syntax_phases.ML"
   2.156 -    "Syntax/syntax_trans.ML"
   2.157 -    "Syntax/term_position.ML"
   2.158 -    "Syntax/type_annotation.ML"
   2.159 -    "System/bash.ML"
   2.160 -    "System/command_line.ML"
   2.161 -    "System/distribution.ML"
   2.162 -    "System/invoke_scala.ML"
   2.163 -    "System/isabelle_process.ML"
   2.164 -    "System/isabelle_system.ML"
   2.165 -    "System/message_channel.ML"
   2.166 -    "System/options.ML"
   2.167 -    "System/system_channel.ML"
   2.168 -    "Thy/document_antiquotations.ML"
   2.169 -    "Thy/html.ML"
   2.170 -    "Thy/latex.ML"
   2.171 -    "Thy/markdown.ML"
   2.172 -    "Thy/present.ML"
   2.173 -    "Thy/term_style.ML"
   2.174 -    "Thy/thy_header.ML"
   2.175 -    "Thy/thy_info.ML"
   2.176 -    "Thy/thy_output.ML"
   2.177 -    "Thy/thy_syntax.ML"
   2.178 -    "Tools/bibtex.ML"
   2.179 -    "Tools/build.ML"
   2.180 -    "Tools/class_deps.ML"
   2.181 -    "Tools/debugger.ML"
   2.182 -    "Tools/find_consts.ML"
   2.183 -    "Tools/find_theorems.ML"
   2.184 -    "Tools/jedit.ML"
   2.185 -    "Tools/named_theorems.ML"
   2.186 -    "Tools/named_thms.ML"
   2.187 -    "Tools/plugin.ML"
   2.188 -    "Tools/print_operation.ML"
   2.189 -    "Tools/rail.ML"
   2.190 -    "Tools/rule_insts.ML"
   2.191 -    "Tools/simplifier_trace.ML"
   2.192 -    "Tools/thm_deps.ML"
   2.193 -    "Tools/thy_deps.ML"
   2.194 -    "assumption.ML"
   2.195 -    "axclass.ML"
   2.196 -    "config.ML"
   2.197 -    "conjunction.ML"
   2.198 -    "consts.ML"
   2.199 -    "context.ML"
   2.200 -    "context_position.ML"
   2.201 -    "conv.ML"
   2.202 -    "defs.ML"
   2.203 -    "drule.ML"
   2.204 -    "envir.ML"
   2.205 -    "facts.ML"
   2.206 -    "global_theory.ML"
   2.207 -    "goal.ML"
   2.208 -    "goal_display.ML"
   2.209 -    "item_net.ML"
   2.210 -    "library.ML"
   2.211 -    "logic.ML"
   2.212 -    "more_pattern.ML"
   2.213 -    "more_thm.ML"
   2.214 -    "more_unify.ML"
   2.215 -    "morphism.ML"
   2.216 -    "name.ML"
   2.217 -    "net.ML"
   2.218 -    "par_tactical.ML"
   2.219 -    "pattern.ML"
   2.220 -    "primitive_defs.ML"
   2.221 -    "proofterm.ML"
   2.222 -    "pure_syn.ML"
   2.223 -    "pure_thy.ML"
   2.224 -    "raw_simplifier.ML"
   2.225 -    "search.ML"
   2.226 -    "sign.ML"
   2.227 -    "simplifier.ML"
   2.228 -    "skip_proof.ML"
   2.229 -    "sorts.ML"
   2.230 -    "tactic.ML"
   2.231 -    "tactical.ML"
   2.232 -    "term.ML"
   2.233 -    "term_ord.ML"
   2.234 -    "term_sharing.ML"
   2.235 -    "term_subst.ML"
   2.236 -    "term_xml.ML"
   2.237 -    "theory.ML"
   2.238 -    "thm.ML"
   2.239 -    "type.ML"
   2.240 -    "type_infer.ML"
   2.241 -    "type_infer_context.ML"
   2.242 -    "unify.ML"
   2.243 -    "variable.ML"
   2.244 +  files "ROOT.ML"
     3.1 --- a/src/Pure/Tools/build.scala	Tue Apr 05 14:59:00 2016 +0200
     3.2 +++ b/src/Pure/Tools/build.scala	Tue Apr 05 15:27:11 2016 +0200
     3.3 @@ -173,7 +173,11 @@
     3.4              val syntax = thy_deps.syntax.asInstanceOf[Outer_Syntax]
     3.5  
     3.6              val theory_files = thy_deps.deps.map(dep => Path.explode(dep.name.node))
     3.7 -            val loaded_files = if (inlined_files) thy_deps.loaded_files else Nil
     3.8 +            val loaded_files =
     3.9 +              if (inlined_files)
    3.10 +                thy_deps.loaded_files :::
    3.11 +                  (if (Sessions.is_pure(name)) ML_Root.read(info.dir).map(_._2) else Nil)
    3.12 +              else Nil
    3.13  
    3.14              val all_files =
    3.15                (theory_files ::: loaded_files :::
     4.1 --- a/src/Pure/build-jars	Tue Apr 05 14:59:00 2016 +0200
     4.2 +++ b/src/Pure/build-jars	Tue Apr 05 15:27:11 2016 +0200
     4.3 @@ -54,6 +54,7 @@
     4.4    Isar/parse.scala
     4.5    Isar/token.scala
     4.6    ML/ml_lex.scala
     4.7 +  ML/ml_root.scala
     4.8    ML/ml_syntax.scala
     4.9    PIDE/batch_session.scala
    4.10    PIDE/command.scala