author  wenzelm 
Thu, 06 Mar 2008 20:17:49 +0100  
changeset 26219  2d026932f710 
parent 26214  73ed8cb8ac4d 
child 26224  5b4e5af10de6 
permissions  rwrr 
2431  1 
# 
4518  2 
# $Id$ 
2431  3 
# 
4518  4 
# IsaMakefile for Pure 
2431  5 
# 
6 

4518  7 
## targets 
8 

9 
default: Pure 

10 
images: Pure 

24880
c827d25b2983
added PureProofGeneral target (dummy session with outer syntax keyword initialization);
wenzelm
parents:
24830
diff
changeset

11 
test: RAW PureProofGeneral 
4518  12 
all: images test 
13 

14 

15 
## global settings 

16 

17 
SRC = $(ISABELLE_HOME)/src 

3118  18 
OUT = $(ISABELLE_OUTPUT) 
4518  19 
LOG = $(OUT)/log 
20 

2431  21 

4518  22 
## Pure 
23 

17802
f3b1ca16cebd
moved susp.ML, lazy_seq.ML, lazy_scan.ML to HOL/Import;
wenzelm
parents:
17338
diff
changeset

24 
Pure: $(OUT)/Pure$(ML_SUFFIX) 
2431  25 

26214  26 
$(OUT)/Pure$(ML_SUFFIX): CPure.thy General/ROOT.ML General/alist.ML \ 
27 
General/balanced_tree.ML General/basics.ML General/buffer.ML \ 

28 
General/file.ML General/graph.ML General/heap.ML General/history.ML \ 

29 
General/integer.ML General/markup.ML General/name_space.ML \ 

30 
General/ord_list.ML General/output.ML General/path.ML \ 

31 
General/position.ML General/pretty.ML General/print_mode.ML \ 

32 
General/scan.ML General/secure.ML General/seq.ML General/source.ML \ 

33 
General/stack.ML General/susp.ML General/symbol.ML General/table.ML \ 

34 
General/url.ML General/xml.ML Isar/ROOT.ML Isar/antiquote.ML \ 

35 
Isar/args.ML Isar/attrib.ML Isar/auto_bind.ML Isar/calculation.ML \ 

36 
Isar/class.ML Isar/code.ML Isar/code_unit.ML Isar/constdefs.ML \ 

26097
943582a2d1e2
removed General/system_process.ML (back to multithreaded version);
wenzelm
parents:
26077
diff
changeset

37 
Isar/context_rules.ML Isar/element.ML Isar/find_theorems.ML \ 
943582a2d1e2
removed General/system_process.ML (back to multithreaded version);
wenzelm
parents:
26077
diff
changeset

38 
Isar/instance.ML Isar/isar_cmd.ML Isar/isar_syn.ML \ 
943582a2d1e2
removed General/system_process.ML (back to multithreaded version);
wenzelm
parents:
26077
diff
changeset

39 
Isar/local_defs.ML Isar/local_syntax.ML Isar/local_theory.ML \ 
943582a2d1e2
removed General/system_process.ML (back to multithreaded version);
wenzelm
parents:
26077
diff
changeset

40 
Isar/locale.ML Isar/method.ML Isar/net_rules.ML Isar/object_logic.ML \ 
943582a2d1e2
removed General/system_process.ML (back to multithreaded version);
wenzelm
parents:
26077
diff
changeset

41 
Isar/obtain.ML Isar/outer_keyword.ML Isar/outer_lex.ML \ 
943582a2d1e2
removed General/system_process.ML (back to multithreaded version);
wenzelm
parents:
26077
diff
changeset

42 
Isar/outer_parse.ML Isar/outer_syntax.ML Isar/proof.ML \ 
943582a2d1e2
removed General/system_process.ML (back to multithreaded version);
wenzelm
parents:
26077
diff
changeset

43 
Isar/proof_context.ML Isar/proof_display.ML Isar/proof_history.ML \ 
943582a2d1e2
removed General/system_process.ML (back to multithreaded version);
wenzelm
parents:
26077
diff
changeset

44 
Isar/rule_cases.ML Isar/rule_insts.ML Isar/session.ML \ 
943582a2d1e2
removed General/system_process.ML (back to multithreaded version);
wenzelm
parents:
26077
diff
changeset

45 
Isar/skip_proof.ML Isar/spec_parse.ML Isar/specification.ML \ 
943582a2d1e2
removed General/system_process.ML (back to multithreaded version);
wenzelm
parents:
26077
diff
changeset

46 
Isar/subclass.ML Isar/theory_target.ML Isar/toplevel.ML \ 
943582a2d1e2
removed General/system_process.ML (back to multithreaded version);
wenzelm
parents:
26077
diff
changeset

47 
MLSystems/alice.ML MLSystems/exn.ML MLSystems/multithreading.ML \ 
943582a2d1e2
removed General/system_process.ML (back to multithreaded version);
wenzelm
parents:
26077
diff
changeset

48 
MLSystems/multithreading_polyml.ML MLSystems/overloading_smlnj.ML \ 
943582a2d1e2
removed General/system_process.ML (back to multithreaded version);
wenzelm
parents:
26077
diff
changeset

49 
MLSystems/polyml4.1.3.ML MLSystems/polyml4.1.4.ML \ 
26214  50 
MLSystems/polyml4.2.0.ML MLSystems/polyml5.0.ML \ 
51 
MLSystems/polyml_common.ML MLSystems/polyml.ML \ 

52 
MLSystems/poplogml.ML MLSystems/proper_int.ML MLSystems/smlnj.ML \ 

26219  53 
MLSystems/system_shell.ML MLSystems/time_limit.ML \ 
54 
MLSystems/universal.ML ML/ml_context.ML ML/ml_lex.ML ML/ml_parse.ML \ 

55 
ML/ml_syntax.ML Proof/extraction.ML Proof/proof_rewrite_rules.ML \ 

56 
Proof/proof_syntax.ML Proof/proofchecker.ML Proof/reconstruct.ML \ 

57 
ProofGeneral/ROOT.ML ProofGeneral/pgip.ML ProofGeneral/pgip_input.ML \ 

26097
943582a2d1e2
removed General/system_process.ML (back to multithreaded version);
wenzelm
parents:
26077
diff
changeset

58 
ProofGeneral/pgip_isabelle.ML ProofGeneral/pgip_markup.ML \ 
943582a2d1e2
removed General/system_process.ML (back to multithreaded version);
wenzelm
parents:
26077
diff
changeset

59 
ProofGeneral/pgip_output.ML ProofGeneral/pgip_parser.ML \ 
943582a2d1e2
removed General/system_process.ML (back to multithreaded version);
wenzelm
parents:
26077
diff
changeset

60 
ProofGeneral/pgip_tests.ML ProofGeneral/pgip_types.ML \ 
943582a2d1e2
removed General/system_process.ML (back to multithreaded version);
wenzelm
parents:
26077
diff
changeset

61 
ProofGeneral/pgml_isabelle.ML ProofGeneral/preferences.ML \ 
943582a2d1e2
removed General/system_process.ML (back to multithreaded version);
wenzelm
parents:
26077
diff
changeset

62 
ProofGeneral/proof_general_emacs.ML \ 
943582a2d1e2
removed General/system_process.ML (back to multithreaded version);
wenzelm
parents:
26077
diff
changeset

63 
ProofGeneral/proof_general_pgip.ML Pure.thy ROOT.ML Syntax/ast.ML \ 
943582a2d1e2
removed General/system_process.ML (back to multithreaded version);
wenzelm
parents:
26077
diff
changeset

64 
Syntax/lexicon.ML Syntax/mixfix.ML Syntax/parser.ML \ 
943582a2d1e2
removed General/system_process.ML (back to multithreaded version);
wenzelm
parents:
26077
diff
changeset

65 
Syntax/printer.ML Syntax/simple_syntax.ML Syntax/syn_ext.ML \ 
943582a2d1e2
removed General/system_process.ML (back to multithreaded version);
wenzelm
parents:
26077
diff
changeset

66 
Syntax/syn_trans.ML Syntax/syntax.ML Syntax/type_ext.ML Thy/html.ML \ 
943582a2d1e2
removed General/system_process.ML (back to multithreaded version);
wenzelm
parents:
26077
diff
changeset

67 
Thy/latex.ML Thy/present.ML Thy/term_style.ML Thy/thm_database.ML \ 
943582a2d1e2
removed General/system_process.ML (back to multithreaded version);
wenzelm
parents:
26077
diff
changeset

68 
Thy/thm_deps.ML Thy/thy_edit.ML Thy/thy_header.ML Thy/thy_info.ML \ 
943582a2d1e2
removed General/system_process.ML (back to multithreaded version);
wenzelm
parents:
26077
diff
changeset

69 
Thy/thy_load.ML Thy/thy_output.ML Tools/ROOT.ML Tools/invoke.ML \ 
943582a2d1e2
removed General/system_process.ML (back to multithreaded version);
wenzelm
parents:
26077
diff
changeset

70 
Tools/isabelle_process.ML Tools/named_thms.ML Tools/xml_syntax.ML \ 
943582a2d1e2
removed General/system_process.ML (back to multithreaded version);
wenzelm
parents:
26077
diff
changeset

71 
assumption.ML axclass.ML codegen.ML compress.ML config.ML \ 
943582a2d1e2
removed General/system_process.ML (back to multithreaded version);
wenzelm
parents:
26077
diff
changeset

72 
conjunction.ML consts.ML context.ML conv.ML defs.ML display.ML \ 
943582a2d1e2
removed General/system_process.ML (back to multithreaded version);
wenzelm
parents:
26077
diff
changeset

73 
drule.ML envir.ML fact_index.ML goal.ML interpretation.ML library.ML \ 
943582a2d1e2
removed General/system_process.ML (back to multithreaded version);
wenzelm
parents:
26077
diff
changeset

74 
logic.ML meta_simplifier.ML more_thm.ML morphism.ML name.ML net.ML \ 
943582a2d1e2
removed General/system_process.ML (back to multithreaded version);
wenzelm
parents:
26077
diff
changeset

75 
old_goals.ML pattern.ML primitive_defs.ML proofterm.ML pure_setup.ML \ 
943582a2d1e2
removed General/system_process.ML (back to multithreaded version);
wenzelm
parents:
26077
diff
changeset

76 
pure_thy.ML search.ML sign.ML simplifier.ML sorts.ML subgoal.ML \ 
943582a2d1e2
removed General/system_process.ML (back to multithreaded version);
wenzelm
parents:
26077
diff
changeset

77 
tactic.ML tctical.ML term.ML term_subst.ML theory.ML thm.ML type.ML \ 
943582a2d1e2
removed General/system_process.ML (back to multithreaded version);
wenzelm
parents:
26077
diff
changeset

78 
type_infer.ML unify.ML variable.ML 
2431  79 
@./mk 
80 

4518  81 

10102  82 
## special targets 
83 

24880
c827d25b2983
added PureProofGeneral target (dummy session with outer syntax keyword initialization);
wenzelm
parents:
24830
diff
changeset

84 
PureProofGeneral: Pure $(LOG)/PureProofGeneral.gz 
c827d25b2983
added PureProofGeneral target (dummy session with outer syntax keyword initialization);
wenzelm
parents:
24830
diff
changeset

85 

c827d25b2983
added PureProofGeneral target (dummy session with outer syntax keyword initialization);
wenzelm
parents:
24830
diff
changeset

86 
$(LOG)/PureProofGeneral.gz: $(OUT)/Pure$(ML_SUFFIX) ProofGeneral/proof_general_keywords.ML 
c827d25b2983
added PureProofGeneral target (dummy session with outer syntax keyword initialization);
wenzelm
parents:
24830
diff
changeset

87 
@$(ISATOOL) usedir f proof_general_keywords.ML $(OUT)/Pure ProofGeneral 
c827d25b2983
added PureProofGeneral target (dummy session with outer syntax keyword initialization);
wenzelm
parents:
24830
diff
changeset

88 

c827d25b2983
added PureProofGeneral target (dummy session with outer syntax keyword initialization);
wenzelm
parents:
24830
diff
changeset

89 

21995  90 
RAW: $(OUT)/RAW 
4518  91 

26214  92 
$(OUT)/RAW: MLSystems/alice.ML MLSystems/exn.ML \ 
93 
MLSystems/multithreading.ML MLSystems/multithreading_polyml.ML \ 

94 
MLSystems/overloading_smlnj.ML MLSystems/polyml4.1.3.ML \ 

95 
MLSystems/polyml4.1.4.ML MLSystems/polyml4.2.0.ML \ 

96 
MLSystems/polyml5.0.ML MLSystems/polyml_common.ML \ 

97 
MLSystems/polyml.ML MLSystems/poplogml.ML MLSystems/proper_int.ML \ 

26219  98 
MLSystems/smlnj.ML MLSystems/system_shell.ML \ 
99 
MLSystems/time_limit.ML MLSystems/universal.ML 

3774  100 
@./mk r 
101 

4518  102 

103 
## clean 

4441  104 

105 
clean: 

24880
c827d25b2983
added PureProofGeneral target (dummy session with outer syntax keyword initialization);
wenzelm
parents:
24830
diff
changeset

106 
@rm f $(OUT)/Pure$(ML_SUFFIX) $(LOG)/Pure.gz $(LOG)/PureProofGeneral.gz \ 
c827d25b2983
added PureProofGeneral target (dummy session with outer syntax keyword initialization);
wenzelm
parents:
24830
diff
changeset

107 
$(OUT)/RAW $(LOG)/RAW.gz 