author  wenzelm 
Mon, 29 Dec 2008 20:06:31 +0100  
changeset 29202  2454172eddae 
parent 29190  89217ccfd130 
child 29252  ea97aa6aeba2 
permissions  rwrr 
2431  1 
# 
4518  2 
# IsaMakefile for Pure 
2431  3 
# 
4 

4518  5 
## targets 
6 

7 
default: Pure 

8 
images: Pure 

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

9 
test: RAW PureProofGeneral 
4518  10 
all: images test 
11 

12 

13 
## global settings 

14 

15 
SRC = $(ISABELLE_HOME)/src 

3118  16 
OUT = $(ISABELLE_OUTPUT) 
4518  17 
LOG = $(OUT)/log 
18 

2431  19 

4518  20 
## Pure 
21 

27204  22 
Pure: $(OUT)/Pure 
2431  23 

28632  24 
$(OUT)/Pure: Concurrent/ROOT.ML Concurrent/future.ML \ 
25 
Concurrent/mailbox.ML Concurrent/par_list.ML \ 

29118  26 
Concurrent/par_list_dummy.ML Concurrent/simple_thread.ML \ 
27 
Concurrent/synchronized.ML Concurrent/task_queue.ML General/ROOT.ML \ 

28 
General/alist.ML General/balanced_tree.ML General/basics.ML \ 

29 
General/buffer.ML General/file.ML General/graph.ML General/heap.ML \ 

30 
General/integer.ML General/lazy.ML General/markup.ML \ 

31 
General/name_space.ML General/ord_list.ML General/output.ML \ 

32 
General/path.ML General/position.ML General/pretty.ML \ 

33 
General/print_mode.ML General/properties.ML General/queue.ML \ 

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

35 
General/stack.ML General/symbol.ML General/symbol_pos.ML \ 

36 
General/table.ML General/url.ML General/xml.ML General/yxml.ML \ 

37 
Isar/ROOT.ML Isar/antiquote.ML Isar/args.ML Isar/attrib.ML \ 

38 
Isar/auto_bind.ML Isar/calculation.ML Isar/class.ML Isar/code.ML \ 

39 
Isar/code_unit.ML Isar/constdefs.ML Isar/context_rules.ML \ 

40 
Isar/element.ML Isar/expression.ML Isar/find_theorems.ML \ 

41 
Isar/instance.ML Isar/isar.ML Isar/isar_cmd.ML Isar/isar_syn.ML \ 

42 
Isar/local_defs.ML Isar/local_syntax.ML Isar/local_theory.ML \ 

43 
Isar/locale.ML Isar/method.ML Isar/net_rules.ML Isar/new_locale.ML \ 

28673
d746a8c12c43
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
28632
diff
changeset

44 
Isar/object_logic.ML Isar/obtain.ML Isar/outer_keyword.ML \ 
d746a8c12c43
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
28632
diff
changeset

45 
Isar/outer_lex.ML Isar/outer_parse.ML Isar/outer_syntax.ML \ 
d746a8c12c43
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
28632
diff
changeset

46 
Isar/overloading.ML Isar/proof.ML Isar/proof_context.ML \ 
d746a8c12c43
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
28632
diff
changeset

47 
Isar/proof_display.ML Isar/proof_node.ML Isar/rule_cases.ML \ 
d746a8c12c43
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
28632
diff
changeset

48 
Isar/rule_insts.ML Isar/session.ML Isar/skip_proof.ML \ 
d746a8c12c43
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
28632
diff
changeset

49 
Isar/spec_parse.ML Isar/specification.ML Isar/subclass.ML \ 
d746a8c12c43
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
28632
diff
changeset

50 
Isar/theory_target.ML Isar/toplevel.ML MLSystems/alice.ML \ 
d746a8c12c43
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
28632
diff
changeset

51 
MLSystems/exn.ML MLSystems/install_pp_polyml.ML \ 
d746a8c12c43
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
28632
diff
changeset

52 
MLSystems/ml_name_space.ML MLSystems/multithreading.ML \ 
d746a8c12c43
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
28632
diff
changeset

53 
MLSystems/mosml.ML MLSystems/multithreading_polyml.ML \ 
d746a8c12c43
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
28632
diff
changeset

54 
MLSystems/overloading_smlnj.ML MLSystems/polyml4.1.3.ML \ 
d746a8c12c43
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
28632
diff
changeset

55 
MLSystems/polyml4.1.4.ML MLSystems/polyml4.2.0.ML \ 
d746a8c12c43
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
28632
diff
changeset

56 
MLSystems/polyml5.0.ML MLSystems/polyml5.1.ML \ 
d746a8c12c43
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
28632
diff
changeset

57 
MLSystems/polyml_common.ML MLSystems/polyml.ML \ 
d746a8c12c43
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
28632
diff
changeset

58 
MLSystems/polyml_old_compiler4.ML \ 
27204  59 
MLSystems/polyml_old_compiler5.ML MLSystems/proper_int.ML \ 
60 
MLSystems/smlnj.ML MLSystems/system_shell.ML \ 

28146  61 
MLSystems/time_limit.ML MLSystems/thread_dummy.ML \ 
62 
MLSystems/universal.ML ML/ml_context.ML ML/ml_antiquote.ML \ 

63 
ML/ml_lex.ML ML/ml_parse.ML ML/ml_syntax.ML ML/ml_thms.ML \ 

64 
Proof/extraction.ML Proof/proof_rewrite_rules.ML \ 

27339  65 
Proof/proof_syntax.ML Proof/proofchecker.ML Proof/reconstruct.ML \ 
66 
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

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

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

69 
ProofGeneral/pgip_tests.ML ProofGeneral/pgip_types.ML \ 
28030  70 
ProofGeneral/preferences.ML ProofGeneral/proof_general_emacs.ML \ 
26097
943582a2d1e2
removed General/system_process.ML (back to multithreaded version);
wenzelm
parents:
26077
diff
changeset

71 
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

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

73 
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

74 
Syntax/syn_trans.ML Syntax/syntax.ML Syntax/type_ext.ML Thy/html.ML \ 
26419
945d8d7a66ec
removed obsolete Thy/thm_database.ML (cf. ML/ml_context.ML);
wenzelm
parents:
26384
diff
changeset

75 
Thy/latex.ML Thy/present.ML Thy/term_style.ML Thy/thm_deps.ML \ 
945d8d7a66ec
removed obsolete Thy/thm_database.ML (cf. ML/ml_context.ML);
wenzelm
parents:
26384
diff
changeset

76 
Thy/thy_edit.ML Thy/thy_header.ML Thy/thy_info.ML Thy/thy_load.ML \ 
29118  77 
Thy/thy_output.ML Tools/ROOT.ML Tools/invoke.ML \ 
78 
Tools/isabelle_process.ML Tools/named_thms.ML Tools/xml_syntax.ML \ 

79 
assumption.ML axclass.ML codegen.ML config.ML conjunction.ML \ 

80 
consts.ML context.ML context_position.ML conv.ML defs.ML display.ML \ 

81 
drule.ML envir.ML facts.ML goal.ML interpretation.ML library.ML \ 

82 
logic.ML meta_simplifier.ML more_thm.ML morphism.ML name.ML net.ML \ 

83 
old_goals.ML pattern.ML primitive_defs.ML proofterm.ML pure_setup.ML \ 

84 
pure_thy.ML search.ML sign.ML simplifier.ML sorts.ML subgoal.ML \ 

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

86 
type_infer.ML unify.ML variable.ML ../Tools/quickcheck.ML 

2431  87 
@./mk 
88 

4518  89 

10102  90 
## special targets 
91 

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

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

93 

27204  94 
$(LOG)/PureProofGeneral.gz: $(OUT)/Pure ProofGeneral/proof_general_keywords.ML 
28500  95 
@$(ISABELLE_TOOL) usedir f proof_general_keywords.ML $(OUT)/Pure ProofGeneral 
24880
c827d25b2983
added PureProofGeneral target (dummy session with outer syntax keyword initialization);
wenzelm
parents:
24830
diff
changeset

96 

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

97 

21995  98 
RAW: $(OUT)/RAW 
4518  99 

28266  100 
$(OUT)/RAW: MLSystems/alice.ML MLSystems/exn.ML \ 
101 
MLSystems/ml_name_space.ML MLSystems/multithreading.ML \ 

102 
MLSystems/mosml.ML MLSystems/multithreading_polyml.ML \ 

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

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

105 
MLSystems/polyml5.0.ML MLSystems/polyml5.1.ML \ 

106 
MLSystems/polyml_common.ML MLSystems/polyml.ML \ 

107 
MLSystems/polyml_old_compiler4.ML \ 

108 
MLSystems/polyml_old_compiler5.ML MLSystems/proper_int.ML \ 

109 
MLSystems/smlnj.ML MLSystems/system_shell.ML \ 

110 
MLSystems/time_limit.ML MLSystems/thread_dummy.ML \ 

28146  111 
MLSystems/universal.ML 
3774  112 
@./mk r 
113 

4518  114 

115 
## clean 

4441  116 

117 
clean: 

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

119 
$(OUT)/RAW $(LOG)/RAW.gz 
27902  120 

121 

122 
## Scala material 

123 

29202  124 
SCALA_FILES = General/event_bus.scala General/markup.scala \ 
125 
General/position.scala General/swing.scala General/symbol.scala \ 

126 
General/xml.scala General/yxml.scala Isar/isar.scala \ 

127 
Thy/thy_header.scala Tools/isabelle_process.scala \ 

128 
Tools/isabelle_syntax.scala Tools/isabelle_system.scala 

27950
dbb93a5e6e6a
added Tools/isabelle_process.scala, Tools/isabelle_syntax.scala;
wenzelm
parents:
27929
diff
changeset

129 

dbb93a5e6e6a
added Tools/isabelle_process.scala, Tools/isabelle_syntax.scala;
wenzelm
parents:
27929
diff
changeset

130 

27902  131 
SCALA_TARGET = $(ISABELLE_HOME)/lib/classes/Pure.jar 
132 

133 
jar: $(SCALA_TARGET) 

134 

135 
$(SCALA_TARGET): $(SCALA_FILES) 

136 
@rm rf classes && mkdir classes 

27950
dbb93a5e6e6a
added Tools/isabelle_process.scala, Tools/isabelle_syntax.scala;
wenzelm
parents:
27929
diff
changeset

137 
scalac deprecation d classes target jvm1.5 $(SCALA_FILES) 
27925  138 
scaladoc d classes $(SCALA_FILES) 
28295  139 
@cp $(SCALA_FILES) classes/isabelle 
27902  140 
@mkdir p `dirname $@` 
27922
ddf74e16ab01
jar target: removed jvmpath  does not work on Linux!?
wenzelm
parents:
27920
diff
changeset

141 
@cd classes; jar cf $@ isabelle 
28003  142 
@rm rf classes 
27902  143 

144 
cleanjar: 

145 
@rm f $(SCALA_TARGET) 