--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML/ml_root.scala Tue Apr 05 15:27:11 2016 +0200
@@ -0,0 +1,54 @@
+/* Title: Pure/ML/ml_root.scala
+ Author: Makarius
+
+Support for ML project ROOT file, with imitation of ML "use" commands.
+*/
+
+package isabelle
+
+
+object ML_Root
+{
+ /* parser */
+
+ val ROOT_ML = Path.explode("ROOT.ML")
+
+ val USE = "use"
+ val USE_DEBUG = "use_debug"
+ val USE_NO_DEBUG = "use_no_debug"
+ val USE_THY = "use_thy"
+
+ lazy val syntax =
+ Outer_Syntax.init() + ";" +
+ (USE, Some((Keyword.THY_LOAD, Nil)), None) +
+ (USE_DEBUG, Some((Keyword.THY_LOAD, Nil)), None) +
+ (USE_NO_DEBUG, Some((Keyword.THY_LOAD, Nil)), None) +
+ (USE_THY, Some((Keyword.THY_LOAD, Nil)), None)
+
+ private object Parser extends Parse.Parser
+ {
+ val entry: Parser[(String, String)] =
+ (command(USE) | command(USE_DEBUG) | command(USE_NO_DEBUG) | command(USE_THY)) ~!
+ (string ~ $$$(";")) ^^ { case a ~ (b ~ _) => (a, b) }
+
+ def parse(in: Token.Reader): ParseResult[List[(String, String)]] =
+ parse_all(rep(entry), in)
+ }
+
+ def read(dir: Path): List[(String, Path)] =
+ {
+ val root = dir + ROOT_ML
+
+ val toks = Token.explode(syntax.keywords, File.read(root))
+ val start = Token.Pos.file(root.implode)
+
+ Parser.parse(Token.reader(toks, start)) match {
+ case Parser.Success(entries, _) =>
+ for ((a, b) <- entries) yield {
+ val path = dir + Path.explode(b)
+ (a, if (a == USE_THY) Resources.thy_path(path) else path)
+ }
+ case bad => error(bad.toString)
+ }
+ }
+}
--- a/src/Pure/ROOT Tue Apr 05 14:59:00 2016 +0200
+++ b/src/Pure/ROOT Tue Apr 05 15:27:11 2016 +0200
@@ -2,240 +2,4 @@
session Pure =
global_theories Pure
- files
- "Concurrent/cache.ML"
- "Concurrent/counter.ML"
- "Concurrent/event_timer.ML"
- "Concurrent/future.ML"
- "Concurrent/lazy.ML"
- "Concurrent/mailbox.ML"
- "Concurrent/multithreading.ML"
- "Concurrent/par_exn.ML"
- "Concurrent/par_list.ML"
- "Concurrent/single_assignment.ML"
- "Concurrent/standard_thread.ML"
- "Concurrent/synchronized.ML"
- "Concurrent/task_queue.ML"
- "Concurrent/timeout.ML"
- "Concurrent/unsynchronized.ML"
- "General/alist.ML"
- "General/antiquote.ML"
- "General/balanced_tree.ML"
- "General/basics.ML"
- "General/binding.ML"
- "General/buffer.ML"
- "General/change_table.ML"
- "General/completion.ML"
- "General/exn.ML"
- "General/file.ML"
- "General/graph.ML"
- "General/graph_display.ML"
- "General/heap.ML"
- "General/input.ML"
- "General/integer.ML"
- "General/linear_set.ML"
- "General/long_name.ML"
- "General/name_space.ML"
- "General/ord_list.ML"
- "General/output.ML"
- "General/path.ML"
- "General/position.ML"
- "General/pretty.ML"
- "General/print_mode.ML"
- "General/properties.ML"
- "General/queue.ML"
- "General/random.ML"
- "General/same.ML"
- "General/scan.ML"
- "General/seq.ML"
- "General/sha1.ML"
- "General/socket_io.ML"
- "General/source.ML"
- "General/stack.ML"
- "General/symbol.ML"
- "General/symbol_pos.ML"
- "General/table.ML"
- "General/timing.ML"
- "General/url.ML"
- "Isar/args.ML"
- "Isar/attrib.ML"
- "Isar/auto_bind.ML"
- "Isar/bundle.ML"
- "Isar/calculation.ML"
- "Isar/class.ML"
- "Isar/class_declaration.ML"
- "Isar/code.ML"
- "Isar/context_rules.ML"
- "Isar/element.ML"
- "Isar/experiment.ML"
- "Isar/expression.ML"
- "Isar/generic_target.ML"
- "Isar/interpretation.ML"
- "Isar/isar_cmd.ML"
- "Isar/keyword.ML"
- "Isar/local_defs.ML"
- "Isar/local_theory.ML"
- "Isar/locale.ML"
- "Isar/method.ML"
- "Isar/named_target.ML"
- "Isar/object_logic.ML"
- "Isar/obtain.ML"
- "Isar/outer_syntax.ML"
- "Isar/overloading.ML"
- "Isar/parse.ML"
- "Isar/parse_spec.ML"
- "Isar/proof.ML"
- "Isar/proof_context.ML"
- "Isar/proof_display.ML"
- "Isar/proof_node.ML"
- "Isar/rule_cases.ML"
- "Isar/runtime.ML"
- "Isar/spec_rules.ML"
- "Isar/specification.ML"
- "Isar/subgoal.ML"
- "Isar/token.ML"
- "Isar/toplevel.ML"
- "Isar/typedecl.ML"
- "ML/exn_debugger.ML"
- "ML/exn_properties.ML"
- "ML/ml_antiquotation.ML"
- "ML/ml_antiquotations.ML"
- "ML/ml_compiler.ML"
- "ML/ml_compiler0.ML"
- "ML/ml_compiler1.ML"
- "ML/ml_compiler2.ML"
- "ML/ml_context.ML"
- "ML/ml_debugger.ML"
- "ML/ml_env.ML"
- "ML/ml_file.ML"
- "ML/ml_heap.ML"
- "ML/ml_lex.ML"
- "ML/ml_name_space.ML"
- "ML/ml_options.ML"
- "ML/ml_pervasive_final.ML"
- "ML/ml_pervasive_initial.ML"
- "ML/ml_pp.ML"
- "ML/ml_pretty.ML"
- "ML/ml_profiling.ML"
- "ML/ml_statistics.ML"
- "ML/ml_syntax.ML"
- "ML/ml_system.ML"
- "ML/ml_thms.ML"
- "PIDE/active.ML"
- "PIDE/command.ML"
- "PIDE/command_span.ML"
- "PIDE/document.ML"
- "PIDE/document_id.ML"
- "PIDE/execution.ML"
- "PIDE/markup.ML"
- "PIDE/protocol.ML"
- "PIDE/protocol_message.ML"
- "PIDE/query_operation.ML"
- "PIDE/resources.ML"
- "PIDE/session.ML"
- "PIDE/xml.ML"
- "PIDE/yxml.ML"
- "Proof/extraction.ML"
- "Proof/proof_checker.ML"
- "Proof/proof_rewrite_rules.ML"
- "Proof/proof_syntax.ML"
- "Proof/reconstruct.ML"
- "ROOT.ML"
- "Syntax/ast.ML"
- "Syntax/lexicon.ML"
- "Syntax/local_syntax.ML"
- "Syntax/mixfix.ML"
- "Syntax/parser.ML"
- "Syntax/printer.ML"
- "Syntax/simple_syntax.ML"
- "Syntax/syntax.ML"
- "Syntax/syntax_ext.ML"
- "Syntax/syntax_phases.ML"
- "Syntax/syntax_trans.ML"
- "Syntax/term_position.ML"
- "Syntax/type_annotation.ML"
- "System/bash.ML"
- "System/command_line.ML"
- "System/distribution.ML"
- "System/invoke_scala.ML"
- "System/isabelle_process.ML"
- "System/isabelle_system.ML"
- "System/message_channel.ML"
- "System/options.ML"
- "System/system_channel.ML"
- "Thy/document_antiquotations.ML"
- "Thy/html.ML"
- "Thy/latex.ML"
- "Thy/markdown.ML"
- "Thy/present.ML"
- "Thy/term_style.ML"
- "Thy/thy_header.ML"
- "Thy/thy_info.ML"
- "Thy/thy_output.ML"
- "Thy/thy_syntax.ML"
- "Tools/bibtex.ML"
- "Tools/build.ML"
- "Tools/class_deps.ML"
- "Tools/debugger.ML"
- "Tools/find_consts.ML"
- "Tools/find_theorems.ML"
- "Tools/jedit.ML"
- "Tools/named_theorems.ML"
- "Tools/named_thms.ML"
- "Tools/plugin.ML"
- "Tools/print_operation.ML"
- "Tools/rail.ML"
- "Tools/rule_insts.ML"
- "Tools/simplifier_trace.ML"
- "Tools/thm_deps.ML"
- "Tools/thy_deps.ML"
- "assumption.ML"
- "axclass.ML"
- "config.ML"
- "conjunction.ML"
- "consts.ML"
- "context.ML"
- "context_position.ML"
- "conv.ML"
- "defs.ML"
- "drule.ML"
- "envir.ML"
- "facts.ML"
- "global_theory.ML"
- "goal.ML"
- "goal_display.ML"
- "item_net.ML"
- "library.ML"
- "logic.ML"
- "more_pattern.ML"
- "more_thm.ML"
- "more_unify.ML"
- "morphism.ML"
- "name.ML"
- "net.ML"
- "par_tactical.ML"
- "pattern.ML"
- "primitive_defs.ML"
- "proofterm.ML"
- "pure_syn.ML"
- "pure_thy.ML"
- "raw_simplifier.ML"
- "search.ML"
- "sign.ML"
- "simplifier.ML"
- "skip_proof.ML"
- "sorts.ML"
- "tactic.ML"
- "tactical.ML"
- "term.ML"
- "term_ord.ML"
- "term_sharing.ML"
- "term_subst.ML"
- "term_xml.ML"
- "theory.ML"
- "thm.ML"
- "type.ML"
- "type_infer.ML"
- "type_infer_context.ML"
- "unify.ML"
- "variable.ML"
+ files "ROOT.ML"
--- a/src/Pure/Tools/build.scala Tue Apr 05 14:59:00 2016 +0200
+++ b/src/Pure/Tools/build.scala Tue Apr 05 15:27:11 2016 +0200
@@ -173,7 +173,11 @@
val syntax = thy_deps.syntax.asInstanceOf[Outer_Syntax]
val theory_files = thy_deps.deps.map(dep => Path.explode(dep.name.node))
- val loaded_files = if (inlined_files) thy_deps.loaded_files else Nil
+ val loaded_files =
+ if (inlined_files)
+ thy_deps.loaded_files :::
+ (if (Sessions.is_pure(name)) ML_Root.read(info.dir).map(_._2) else Nil)
+ else Nil
val all_files =
(theory_files ::: loaded_files :::
--- a/src/Pure/build-jars Tue Apr 05 14:59:00 2016 +0200
+++ b/src/Pure/build-jars Tue Apr 05 15:27:11 2016 +0200
@@ -54,6 +54,7 @@
Isar/parse.scala
Isar/token.scala
ML/ml_lex.scala
+ ML/ml_root.scala
ML/ml_syntax.scala
PIDE/batch_session.scala
PIDE/command.scala