# HG changeset patch # User wenzelm # Date 1459862831 -7200 # Node ID d20262cd20e89e727cd5d81f00b98c6b19efd317 # Parent cf03cb9578d4fafaea702da14480d6e97b16413c read Pure file dependencies directly from ROOT.ML; diff -r cf03cb9578d4 -r d20262cd20e8 src/Pure/ML/ml_root.scala --- /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) + } + } +} diff -r cf03cb9578d4 -r d20262cd20e8 src/Pure/ROOT --- 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" diff -r cf03cb9578d4 -r d20262cd20e8 src/Pure/Tools/build.scala --- 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 ::: diff -r cf03cb9578d4 -r d20262cd20e8 src/Pure/build-jars --- 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