sub-structural sharing after Syntax.check phase, with global interning of logical entities (the latter is relevant when bypassing default parsing via YXML);
minor tuning;
#
# IsaMakefile for Pure
#
## targets
default: Pure
images: Pure
test: RAW
all: images test
smlnj: all
## global settings
SRC = $(ISABELLE_HOME)/src
OUT = $(ISABELLE_OUTPUT)
LOG = $(OUT)/log
## Pure
BOOTSTRAP_FILES = \
General/exn.ML \
ML-Systems/compiler_polyml-5.2.ML \
ML-Systems/compiler_polyml-5.3.ML \
ML-Systems/ml_name_space.ML \
ML-Systems/ml_pretty.ML \
ML-Systems/multithreading.ML \
ML-Systems/multithreading_polyml.ML \
ML-Systems/overloading_smlnj.ML \
ML-Systems/polyml-5.2.1.ML \
ML-Systems/polyml.ML \
ML-Systems/polyml_common.ML \
ML-Systems/pp_dummy.ML \
ML-Systems/pp_polyml.ML \
ML-Systems/proper_int.ML \
ML-Systems/single_assignment.ML \
ML-Systems/single_assignment_polyml.ML \
ML-Systems/smlnj.ML \
ML-Systems/thread_dummy.ML \
ML-Systems/universal.ML \
ML-Systems/unsynchronized.ML \
ML-Systems/use_context.ML
RAW: $(OUT)/RAW
$(OUT)/RAW: $(BOOTSTRAP_FILES)
@./mk -r
Pure: $(OUT)/Pure
$(OUT)/Pure: $(BOOTSTRAP_FILES) \
Concurrent/bash.ML \
Concurrent/bash_sequential.ML \
Concurrent/cache.ML \
Concurrent/future.ML \
Concurrent/lazy.ML \
Concurrent/lazy_sequential.ML \
Concurrent/mailbox.ML \
Concurrent/par_list.ML \
Concurrent/par_list_sequential.ML \
Concurrent/simple_thread.ML \
Concurrent/single_assignment.ML \
Concurrent/single_assignment_sequential.ML \
Concurrent/synchronized.ML \
Concurrent/synchronized_sequential.ML \
Concurrent/task_queue.ML \
Concurrent/time_limit.ML \
General/alist.ML \
General/antiquote.ML \
General/balanced_tree.ML \
General/basics.ML \
General/binding.ML \
General/buffer.ML \
General/file.ML \
General/graph.ML \
General/heap.ML \
General/integer.ML \
General/linear_set.ML \
General/long_name.ML \
General/markup.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/same.ML \
General/scan.ML \
General/secure.ML \
General/seq.ML \
General/sha1.ML \
General/sha1_polyml.ML \
General/source.ML \
General/stack.ML \
General/symbol.ML \
General/symbol_pos.ML \
General/table.ML \
General/timing.ML \
General/url.ML \
General/xml.ML \
General/yxml.ML \
Isar/args.ML \
Isar/attrib.ML \
Isar/auto_bind.ML \
Isar/calculation.ML \
Isar/class.ML \
Isar/class_declaration.ML \
Isar/code.ML \
Isar/context_rules.ML \
Isar/element.ML \
Isar/expression.ML \
Isar/generic_target.ML \
Isar/isar_cmd.ML \
Isar/isar_syn.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/rule_insts.ML \
Isar/runtime.ML \
Isar/skip_proof.ML \
Isar/spec_rules.ML \
Isar/specification.ML \
Isar/token.ML \
Isar/toplevel.ML \
Isar/typedecl.ML \
ML/install_pp_polyml-5.3.ML \
ML/install_pp_polyml.ML \
ML/ml_antiquote.ML \
ML/ml_compiler.ML \
ML/ml_compiler_polyml-5.3.ML \
ML/ml_context.ML \
ML/ml_env.ML \
ML/ml_lex.ML \
ML/ml_parse.ML \
ML/ml_syntax.ML \
ML/ml_thms.ML \
PIDE/document.ML \
PIDE/isar_document.ML \
Proof/extraction.ML \
Proof/proof_rewrite_rules.ML \
Proof/proof_syntax.ML \
Proof/proofchecker.ML \
Proof/reconstruct.ML \
ProofGeneral/pgip.ML \
ProofGeneral/pgip_input.ML \
ProofGeneral/pgip_isabelle.ML \
ProofGeneral/pgip_markup.ML \
ProofGeneral/pgip_output.ML \
ProofGeneral/pgip_parser.ML \
ProofGeneral/pgip_tests.ML \
ProofGeneral/pgip_types.ML \
ProofGeneral/pgml.ML \
ProofGeneral/preferences.ML \
ProofGeneral/proof_general_emacs.ML \
ProofGeneral/proof_general_pgip.ML \
Pure.thy \
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 \
System/invoke_scala.ML \
System/isabelle_process.ML \
System/isabelle_system.ML \
System/isar.ML \
System/session.ML \
Thy/html.ML \
Thy/latex.ML \
Thy/present.ML \
Thy/rail.ML \
Thy/term_style.ML \
Thy/thm_deps.ML \
Thy/thy_header.ML \
Thy/thy_info.ML \
Thy/thy_load.ML \
Thy/thy_output.ML \
Thy/thy_syntax.ML \
Tools/find_consts.ML \
Tools/find_theorems.ML \
Tools/named_thms.ML \
Tools/xml_syntax.ML \
assumption.ML \
axclass.ML \
codegen.ML \
config.ML \
conjunction.ML \
consts.ML \
context.ML \
context_position.ML \
conv.ML \
defs.ML \
display.ML \
drule.ML \
envir.ML \
facts.ML \
global_theory.ML \
goal.ML \
goal_display.ML \
interpretation.ML \
item_net.ML \
library.ML \
logic.ML \
more_thm.ML \
morphism.ML \
name.ML \
net.ML \
old_term.ML \
pattern.ML \
primitive_defs.ML \
proofterm.ML \
pure_setup.ML \
pure_thy.ML \
raw_simplifier.ML \
search.ML \
sign.ML \
simplifier.ML \
sorts.ML \
subgoal.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
@./mk
## clean
clean:
@rm -f $(OUT)/Pure $(LOG)/Pure.gz $(OUT)/RAW $(LOG)/RAW.gz