author  wenzelm 
Sun, 04 Nov 2007 16:43:28 +0100  
changeset 25272  2dbc2bbe237a 
parent 24914  95cda5dd58d5 
child 25275  76d7f3fd4fb3 
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 

24280  26 
$(OUT)/Pure$(ML_SUFFIX): \ 
24235  27 
CPure.thy General/ROOT.ML General/alist.ML General/balanced_tree.ML \ 
28 
General/basics.ML General/buffer.ML General/file.ML General/graph.ML \ 

24633
0a3a02066244
moved Tools/integer.ML to Pure/General/integer.ML;
wenzelm
parents:
24602
diff
changeset

29 
General/heap.ML General/history.ML General/integer.ML General/markup.ML \ 
24574  30 
General/name_space.ML General/ord_list.ML General/output.ML \ 
31 
General/path.ML General/position.ML General/pretty.ML \ 

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

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

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

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

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

37 
Isar/constdefs.ML Isar/context_rules.ML Isar/element.ML \ 

24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
24689
diff
changeset

38 
Isar/find_theorems.ML Isar/instance.ML Isar/isar_cmd.ML \ 
24574  39 
Isar/isar_syn.ML Isar/local_defs.ML Isar/local_syntax.ML \ 
40 
Isar/local_theory.ML Isar/locale.ML Isar/method.ML Isar/net_rules.ML \ 

41 
Isar/object_logic.ML Isar/obtain.ML Isar/outer_keyword.ML \ 

42 
Isar/outer_lex.ML Isar/outer_parse.ML Isar/outer_syntax.ML \ 

43 
Isar/proof.ML Isar/proof_context.ML Isar/proof_display.ML \ 

44 
Isar/proof_history.ML Isar/rule_cases.ML Isar/rule_insts.ML \ 

45 
Isar/session.ML Isar/skip_proof.ML Isar/spec_parse.ML \ 

24914
95cda5dd58d5
added proper subclass concept; improved class target
haftmann
parents:
24880
diff
changeset

46 
Isar/specification.ML Isar/subclass.ML Isar/theory_target.ML Isar/toplevel.ML \ 
24574  47 
MLSystems/alice.ML MLSystems/exn.ML \ 
24689
ac5b5a6155dd
renamed MLSystems/multithreading_dummy.ML to MLSystems/multithreading.ML;
wenzelm
parents:
24664
diff
changeset

48 
MLSystems/multithreading.ML MLSystems/multithreading_polyml.ML \ 
24235  49 
MLSystems/overloading_smlnj.ML MLSystems/polyml4.1.3.ML \ 
50 
MLSystems/polyml4.1.4.ML MLSystems/polyml5.0.ML \ 

24689
ac5b5a6155dd
renamed MLSystems/multithreading_dummy.ML to MLSystems/multithreading.ML;
wenzelm
parents:
24664
diff
changeset

51 
MLSystems/polyml5.1.ML MLSystems/polymloldbasis.ML \ 
ac5b5a6155dd
renamed MLSystems/multithreading_dummy.ML to MLSystems/multithreading.ML;
wenzelm
parents:
24664
diff
changeset

52 
MLSystems/polymlposix.ML MLSystems/polyml.ML MLSystems/poplogml.ML \ 
ac5b5a6155dd
renamed MLSystems/multithreading_dummy.ML to MLSystems/multithreading.ML;
wenzelm
parents:
24664
diff
changeset

53 
MLSystems/proper_int.ML MLSystems/smlnj.ML MLSystems/time_limit.ML \ 
ac5b5a6155dd
renamed MLSystems/multithreading_dummy.ML to MLSystems/multithreading.ML;
wenzelm
parents:
24664
diff
changeset

54 
ML/ml_context.ML ML/ml_lex.ML ML/ml_parse.ML ML/ml_syntax.ML \ 
ac5b5a6155dd
renamed MLSystems/multithreading_dummy.ML to MLSystems/multithreading.ML;
wenzelm
parents:
24664
diff
changeset

55 
Proof/extraction.ML Proof/proof_rewrite_rules.ML Proof/proof_syntax.ML \ 
ac5b5a6155dd
renamed MLSystems/multithreading_dummy.ML to MLSystems/multithreading.ML;
wenzelm
parents:
24664
diff
changeset

56 
Proof/proofchecker.ML Proof/reconstruct.ML ProofGeneral/ROOT.ML \ 
ac5b5a6155dd
renamed MLSystems/multithreading_dummy.ML to MLSystems/multithreading.ML;
wenzelm
parents:
24664
diff
changeset

57 
ProofGeneral/parsing.ML ProofGeneral/pgip.ML ProofGeneral/pgip_input.ML \ 
ac5b5a6155dd
renamed MLSystems/multithreading_dummy.ML to MLSystems/multithreading.ML;
wenzelm
parents:
24664
diff
changeset

58 
ProofGeneral/pgip_isabelle.ML ProofGeneral/pgip_markup.ML \ 
ac5b5a6155dd
renamed MLSystems/multithreading_dummy.ML to MLSystems/multithreading.ML;
wenzelm
parents:
24664
diff
changeset

59 
ProofGeneral/pgip_output.ML ProofGeneral/pgip_parser.ML \ 
25272  60 
ProofGeneral/pgip_tests.ML ProofGeneral/pgip_types.ML ProofGeneral/pgml_isabelle.ML \ 
24689
ac5b5a6155dd
renamed MLSystems/multithreading_dummy.ML to MLSystems/multithreading.ML;
wenzelm
parents:
24664
diff
changeset

61 
ProofGeneral/preferences.ML ProofGeneral/proof_general_emacs.ML \ 
ac5b5a6155dd
renamed MLSystems/multithreading_dummy.ML to MLSystems/multithreading.ML;
wenzelm
parents:
24664
diff
changeset

62 
ProofGeneral/proof_general_pgip.ML Pure.thy ROOT.ML Syntax/ast.ML \ 
ac5b5a6155dd
renamed MLSystems/multithreading_dummy.ML to MLSystems/multithreading.ML;
wenzelm
parents:
24664
diff
changeset

63 
Syntax/lexicon.ML Syntax/mixfix.ML Syntax/parser.ML Syntax/printer.ML \ 
ac5b5a6155dd
renamed MLSystems/multithreading_dummy.ML to MLSystems/multithreading.ML;
wenzelm
parents:
24664
diff
changeset

64 
Syntax/simple_syntax.ML Syntax/syn_ext.ML Syntax/syn_trans.ML Syntax/syntax.ML\ 
24574  65 
Syntax/type_ext.ML Thy/html.ML Thy/latex.ML Thy/present.ML \ 
66 
Thy/term_style.ML Thy/thm_database.ML Thy/thm_deps.ML Thy/thy_edit.ML \ 

67 
Thy/thy_header.ML Thy/thy_info.ML Thy/thy_load.ML Thy/thy_output.ML \ 

68 
Tools/ROOT.ML Tools/invoke.ML Tools/named_thms.ML Tools/xml_syntax.ML \ 

69 
assumption.ML axclass.ML codegen.ML compress.ML config.ML \ 

70 
conjunction.ML consts.ML context.ML context_position.ML conv.ML \ 

24664  71 
defs.ML display.ML drule.ML envir.ML fact_index.ML goal.ML interpretation.ML \ 
72 
library.ML logic.ML meta_simplifier.ML more_thm.ML morphism.ML name.ML net.ML \ 

24574  73 
old_goals.ML pattern.ML primitive_defs.ML proofterm.ML pure_setup.ML \ 
74 
pure_thy.ML search.ML sign.ML simplifier.ML sorts.ML subgoal.ML \ 

75 
tactic.ML tctical.ML term.ML term_subst.ML theory.ML thm.ML type.ML \ 

76 
type_infer.ML unify.ML variable.ML 

2431  77 
@./mk 
78 

4518  79 

10102  80 
## special targets 
81 

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

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

83 

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

84 
$(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

85 
@$(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

86 

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

87 

21995  88 
RAW: $(OUT)/RAW 
4518  89 

24689
ac5b5a6155dd
renamed MLSystems/multithreading_dummy.ML to MLSystems/multithreading.ML;
wenzelm
parents:
24664
diff
changeset

90 
$(OUT)/RAW: MLSystems/alice.ML MLSystems/exn.ML MLSystems/multithreading.ML \ 
ac5b5a6155dd
renamed MLSystems/multithreading_dummy.ML to MLSystems/multithreading.ML;
wenzelm
parents:
24664
diff
changeset

91 
MLSystems/multithreading_polyml.ML MLSystems/overloading_smlnj.ML \ 
ac5b5a6155dd
renamed MLSystems/multithreading_dummy.ML to MLSystems/multithreading.ML;
wenzelm
parents:
24664
diff
changeset

92 
MLSystems/polyml4.1.3.ML MLSystems/polyml4.1.4.ML \ 
ac5b5a6155dd
renamed MLSystems/multithreading_dummy.ML to MLSystems/multithreading.ML;
wenzelm
parents:
24664
diff
changeset

93 
MLSystems/polyml5.0.ML MLSystems/polyml5.1.ML \ 
ac5b5a6155dd
renamed MLSystems/multithreading_dummy.ML to MLSystems/multithreading.ML;
wenzelm
parents:
24664
diff
changeset

94 
MLSystems/polymloldbasis.ML MLSystems/polymlposix.ML \ 
ac5b5a6155dd
renamed MLSystems/multithreading_dummy.ML to MLSystems/multithreading.ML;
wenzelm
parents:
24664
diff
changeset

95 
MLSystems/polyml.ML MLSystems/poplogml.ML MLSystems/proper_int.ML \ 
ac5b5a6155dd
renamed MLSystems/multithreading_dummy.ML to MLSystems/multithreading.ML;
wenzelm
parents:
24664
diff
changeset

96 
MLSystems/smlnj.ML MLSystems/time_limit.ML 
3774  97 
@./mk r 
98 

4518  99 

100 
## clean 

4441  101 

102 
clean: 

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

103 
@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

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