author  wenzelm 
Mon, 11 Mar 2013 13:28:46 +0100  
changeset 51397  03b586ee5930 
parent 50911  ee7fe4230642 
child 51551  88d1d19fb74f 
permissions  rwrr 
51397
03b586ee5930
support for 'chapter' specifications within session ROOT;
wenzelm
parents:
50911
diff
changeset

1 
chapter Pure 
03b586ee5930
support for 'chapter' specifications within session ROOT;
wenzelm
parents:
50911
diff
changeset

2 

48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48732
diff
changeset

3 
session RAW = 
48916  4 
theories 
48347  5 
files 
6 
"General/exn.ML" 

7 
"MLSystems/compiler_polyml.ML" 

8 
"MLSystems/ml_name_space.ML" 

9 
"MLSystems/ml_pretty.ML" 

10 
"MLSystems/ml_system.ML" 

11 
"MLSystems/multithreading.ML" 

12 
"MLSystems/multithreading_polyml.ML" 

13 
"MLSystems/overloading_smlnj.ML" 

14 
"MLSystems/polyml.ML" 

15 
"MLSystems/pp_dummy.ML" 

16 
"MLSystems/proper_int.ML" 

17 
"MLSystems/single_assignment.ML" 

18 
"MLSystems/single_assignment_polyml.ML" 

19 
"MLSystems/smlnj.ML" 

20 
"MLSystems/thread_dummy.ML" 

21 
"MLSystems/universal.ML" 

22 
"MLSystems/unsynchronized.ML" 

23 
"MLSystems/use_context.ML" 

24 

48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48732
diff
changeset

25 
session Pure = 
48422
9613780a805b
determine source dependencies, relatively to preloaded theories;
wenzelm
parents:
48347
diff
changeset

26 
theories Pure 
48514  27 
files 
28 
"General/exn.ML" 

29 
"MLSystems/compiler_polyml.ML" 

30 
"MLSystems/ml_name_space.ML" 

31 
"MLSystems/ml_pretty.ML" 

32 
"MLSystems/ml_system.ML" 

33 
"MLSystems/multithreading.ML" 

34 
"MLSystems/multithreading_polyml.ML" 

35 
"MLSystems/overloading_smlnj.ML" 

36 
"MLSystems/polyml.ML" 

37 
"MLSystems/pp_dummy.ML" 

38 
"MLSystems/proper_int.ML" 

39 
"MLSystems/single_assignment.ML" 

40 
"MLSystems/single_assignment_polyml.ML" 

41 
"MLSystems/smlnj.ML" 

42 
"MLSystems/thread_dummy.ML" 

43 
"MLSystems/universal.ML" 

44 
"MLSystems/unsynchronized.ML" 

45 
"MLSystems/use_context.ML" 

48347  46 

48514  47 
"Concurrent/bash.ML" 
48 
"Concurrent/bash_sequential.ML" 

49 
"Concurrent/cache.ML" 

50 
"Concurrent/future.ML" 

51 
"Concurrent/lazy.ML" 

52 
"Concurrent/lazy_sequential.ML" 

53 
"Concurrent/mailbox.ML" 

54 
"Concurrent/par_exn.ML" 

55 
"Concurrent/par_list.ML" 

56 
"Concurrent/par_list_sequential.ML" 

57 
"Concurrent/simple_thread.ML" 

58 
"Concurrent/single_assignment.ML" 

59 
"Concurrent/single_assignment_sequential.ML" 

60 
"Concurrent/synchronized.ML" 

61 
"Concurrent/synchronized_sequential.ML" 

62 
"Concurrent/task_queue.ML" 

63 
"Concurrent/time_limit.ML" 

64 
"General/alist.ML" 

65 
"General/antiquote.ML" 

66 
"General/balanced_tree.ML" 

67 
"General/basics.ML" 

68 
"General/binding.ML" 

69 
"General/buffer.ML" 

70 
"General/file.ML" 

71 
"General/graph.ML" 

49561  72 
"General/graph_display.ML" 
48514  73 
"General/heap.ML" 
74 
"General/integer.ML" 

75 
"General/linear_set.ML" 

76 
"General/long_name.ML" 

77 
"General/name_space.ML" 

78 
"General/ord_list.ML" 

79 
"General/output.ML" 

80 
"General/path.ML" 

81 
"General/position.ML" 

82 
"General/pretty.ML" 

83 
"General/print_mode.ML" 

84 
"General/properties.ML" 

85 
"General/queue.ML" 

86 
"General/same.ML" 

87 
"General/scan.ML" 

88 
"General/secure.ML" 

89 
"General/seq.ML" 

90 
"General/sha1.ML" 

91 
"General/sha1_polyml.ML" 

50800
c0fb2839d1a9
recovered buffered sockets from 11f622794ad6  requires Poly/ML 5.5.x;
wenzelm
parents:
50686
diff
changeset

92 
"General/socket_io.ML" 
48514  93 
"General/source.ML" 
94 
"General/stack.ML" 

95 
"General/symbol.ML" 

96 
"General/symbol_pos.ML" 

97 
"General/table.ML" 

98 
"General/timing.ML" 

99 
"General/url.ML" 

100 
"Isar/args.ML" 

101 
"Isar/attrib.ML" 

102 
"Isar/auto_bind.ML" 

103 
"Isar/bundle.ML" 

104 
"Isar/calculation.ML" 

105 
"Isar/class.ML" 

106 
"Isar/class_declaration.ML" 

107 
"Isar/code.ML" 

108 
"Isar/context_rules.ML" 

109 
"Isar/element.ML" 

110 
"Isar/expression.ML" 

111 
"Isar/generic_target.ML" 

112 
"Isar/isar_cmd.ML" 

113 
"Isar/keyword.ML" 

114 
"Isar/local_defs.ML" 

115 
"Isar/local_theory.ML" 

116 
"Isar/locale.ML" 

117 
"Isar/method.ML" 

118 
"Isar/named_target.ML" 

119 
"Isar/object_logic.ML" 

120 
"Isar/obtain.ML" 

121 
"Isar/outer_syntax.ML" 

122 
"Isar/overloading.ML" 

123 
"Isar/parse.ML" 

124 
"Isar/parse_spec.ML" 

125 
"Isar/proof.ML" 

126 
"Isar/proof_context.ML" 

127 
"Isar/proof_display.ML" 

128 
"Isar/proof_node.ML" 

129 
"Isar/rule_cases.ML" 

130 
"Isar/rule_insts.ML" 

131 
"Isar/runtime.ML" 

132 
"Isar/skip_proof.ML" 

133 
"Isar/spec_rules.ML" 

134 
"Isar/specification.ML" 

135 
"Isar/token.ML" 

136 
"Isar/toplevel.ML" 

137 
"Isar/typedecl.ML" 

138 
"ML/install_pp_polyml.ML" 

139 
"ML/ml_antiquote.ML" 

140 
"ML/ml_compiler.ML" 

141 
"ML/ml_compiler_polyml.ML" 

142 
"ML/ml_context.ML" 

143 
"ML/ml_env.ML" 

50911
ee7fe4230642
more explicit treatment of (optional) exception properties, notably for "serial"  avoid conflict with startPosition = offset;
wenzelm
parents:
50800
diff
changeset

144 
"ML/exn_properties_dummy.ML" 
ee7fe4230642
more explicit treatment of (optional) exception properties, notably for "serial"  avoid conflict with startPosition = offset;
wenzelm
parents:
50800
diff
changeset

145 
"ML/exn_properties_polyml.ML" 
48514  146 
"ML/ml_lex.ML" 
147 
"ML/ml_parse.ML" 

50255  148 
"ML/ml_statistics_dummy.ML" 
149 
"ML/ml_statistics_polyml5.5.0.ML" 

48514  150 
"ML/ml_syntax.ML" 
151 
"ML/ml_thms.ML" 

50450
358b6020f8b6
generalized notion of active area, where sendback is just one application;
wenzelm
parents:
50255
diff
changeset

152 
"PIDE/active.ML" 
48514  153 
"PIDE/command.ML" 
154 
"PIDE/document.ML" 

155 
"PIDE/markup.ML" 

156 
"PIDE/protocol.ML" 

157 
"PIDE/xml.ML" 

158 
"PIDE/yxml.ML" 

159 
"Proof/extraction.ML" 

160 
"Proof/proof_checker.ML" 

161 
"Proof/proof_rewrite_rules.ML" 

162 
"Proof/proof_syntax.ML" 

163 
"Proof/reconstruct.ML" 

164 
"ProofGeneral/pgip.ML" 

165 
"ProofGeneral/pgip_input.ML" 

166 
"ProofGeneral/pgip_isabelle.ML" 

167 
"ProofGeneral/pgip_markup.ML" 

168 
"ProofGeneral/pgip_output.ML" 

169 
"ProofGeneral/pgip_parser.ML" 

170 
"ProofGeneral/pgip_tests.ML" 

171 
"ProofGeneral/pgip_types.ML" 

172 
"ProofGeneral/pgml.ML" 

173 
"ProofGeneral/preferences.ML" 

174 
"ProofGeneral/proof_general_emacs.ML" 

175 
"ProofGeneral/proof_general_pgip.ML" 

176 
"ROOT.ML" 

177 
"Syntax/ast.ML" 

178 
"Syntax/lexicon.ML" 

179 
"Syntax/local_syntax.ML" 

180 
"Syntax/mixfix.ML" 

181 
"Syntax/parser.ML" 

182 
"Syntax/printer.ML" 

183 
"Syntax/simple_syntax.ML" 

184 
"Syntax/syntax.ML" 

185 
"Syntax/syntax_ext.ML" 

186 
"Syntax/syntax_phases.ML" 

187 
"Syntax/syntax_trans.ML" 

188 
"Syntax/term_position.ML" 

48681
181b91e1d1c1
prefer general Command_Line.tool wrapper (cf. Scala version);
wenzelm
parents:
48646
diff
changeset

189 
"System/command_line.ML" 
48514  190 
"System/invoke_scala.ML" 
191 
"System/isabelle_process.ML" 

192 
"System/isabelle_system.ML" 

193 
"System/isar.ML" 

194 
"System/options.ML" 

195 
"System/session.ML" 

196 
"System/system_channel.ML" 

197 
"Thy/html.ML" 

198 
"Thy/latex.ML" 

199 
"Thy/present.ML" 

200 
"Thy/rail.ML" 

201 
"Thy/term_style.ML" 

202 
"Thy/thm_deps.ML" 

203 
"Thy/thy_header.ML" 

204 
"Thy/thy_info.ML" 

205 
"Thy/thy_load.ML" 

206 
"Thy/thy_output.ML" 

207 
"Thy/thy_syntax.ML" 

50686  208 
"Tools/build.ML" 
48514  209 
"Tools/named_thms.ML" 
50217
ce1f0602f48e
clarified status of Legacy_XML_Syntax, despite lack of Proofterm_XML;
wenzelm
parents:
50201
diff
changeset

210 
"Tools/legacy_xml_syntax.ML" 
48514  211 
"assumption.ML" 
212 
"axclass.ML" 

213 
"config.ML" 

214 
"conjunction.ML" 

215 
"consts.ML" 

216 
"context.ML" 

217 
"context_position.ML" 

218 
"conv.ML" 

219 
"defs.ML" 

220 
"display.ML" 

221 
"drule.ML" 

222 
"envir.ML" 

223 
"facts.ML" 

224 
"global_theory.ML" 

225 
"goal.ML" 

226 
"goal_display.ML" 

227 
"interpretation.ML" 

228 
"item_net.ML" 

229 
"library.ML" 

230 
"logic.ML" 

231 
"more_thm.ML" 

232 
"morphism.ML" 

233 
"name.ML" 

234 
"net.ML" 

235 
"pattern.ML" 

236 
"primitive_defs.ML" 

237 
"proofterm.ML" 

48879  238 
"pure_syn.ML" 
48514  239 
"pure_thy.ML" 
240 
"raw_simplifier.ML" 

241 
"search.ML" 

242 
"sign.ML" 

243 
"simplifier.ML" 

244 
"sorts.ML" 

245 
"subgoal.ML" 

246 
"tactic.ML" 

247 
"tactical.ML" 

248 
"term.ML" 

249 
"term_ord.ML" 

250 
"term_sharing.ML" 

251 
"term_subst.ML" 

252 
"term_xml.ML" 

253 
"theory.ML" 

254 
"thm.ML" 

255 
"type.ML" 

256 
"type_infer.ML" 

257 
"type_infer_context.ML" 

258 
"unify.ML" 

259 
"variable.ML" 

260 