src/Pure/ROOT
author wenzelm
Tue, 01 Mar 2016 19:42:59 +0100
changeset 62490 39d01eaf5292
parent 62468 d97e13e5ea5b
child 62493 dd154240a53c
permissions -rw-r--r--
ML debugger support in Pure (again, see 3565c9f407ec);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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
f45ccc0d1ace clarified syntax boundary cases and errors;
wenzelm
parents: 48879
diff changeset
     4
  theories
48347
8bb27ab9e841 more explicit treatment of initial Pure sessions;
wenzelm
parents:
diff changeset
     5
  files
62077
e8ae72c26025 clarified ROOT files;
wenzelm
parents: 61926
diff changeset
     6
    "RAW/ROOT_polyml-5.6.ML"
e8ae72c26025 clarified ROOT files;
wenzelm
parents: 61926
diff changeset
     7
    "RAW/ROOT_polyml.ML"
61925
ab52f183f020 clarified directory structure;
wenzelm
parents: 61794
diff changeset
     8
    "RAW/compiler_polyml.ML"
ab52f183f020 clarified directory structure;
wenzelm
parents: 61794
diff changeset
     9
    "RAW/exn.ML"
62459
7a5d88dd8cc9 support only polyml-5.3.0 and polyml-5.6;
wenzelm
parents: 62387
diff changeset
    10
    "RAW/exn_trace.ML"
62460
4b2018eb92e8 clarified;
wenzelm
parents: 62459
diff changeset
    11
    "RAW/exn_trace_raw.ML"
62387
ad3eb2889f9a support for polyml-git ec49a49972c5 (branch FixedPrecisionInt);
wenzelm
parents: 62359
diff changeset
    12
    "RAW/fixed_int_dummy.ML"
61925
ab52f183f020 clarified directory structure;
wenzelm
parents: 61794
diff changeset
    13
    "RAW/ml_compiler_parameters.ML"
ab52f183f020 clarified directory structure;
wenzelm
parents: 61794
diff changeset
    14
    "RAW/ml_compiler_parameters_polyml-5.6.ML"
ab52f183f020 clarified directory structure;
wenzelm
parents: 61794
diff changeset
    15
    "RAW/ml_debugger.ML"
ab52f183f020 clarified directory structure;
wenzelm
parents: 61794
diff changeset
    16
    "RAW/ml_debugger_polyml-5.6.ML"
62467
c1b88e647e2f clarified ML heap operations;
wenzelm
parents: 62460
diff changeset
    17
    "RAW/ml_heap.ML"
c1b88e647e2f clarified ML heap operations;
wenzelm
parents: 62460
diff changeset
    18
    "RAW/ml_heap_polyml-5.3.0.ML"
61925
ab52f183f020 clarified directory structure;
wenzelm
parents: 61794
diff changeset
    19
    "RAW/ml_name_space_polyml-5.6.ML"
ab52f183f020 clarified directory structure;
wenzelm
parents: 61794
diff changeset
    20
    "RAW/ml_name_space_polyml.ML"
ab52f183f020 clarified directory structure;
wenzelm
parents: 61794
diff changeset
    21
    "RAW/ml_parse_tree.ML"
ab52f183f020 clarified directory structure;
wenzelm
parents: 61794
diff changeset
    22
    "RAW/ml_parse_tree_polyml-5.6.ML"
ab52f183f020 clarified directory structure;
wenzelm
parents: 61794
diff changeset
    23
    "RAW/ml_positions.ML"
ab52f183f020 clarified directory structure;
wenzelm
parents: 61794
diff changeset
    24
    "RAW/ml_pretty.ML"
ab52f183f020 clarified directory structure;
wenzelm
parents: 61794
diff changeset
    25
    "RAW/ml_profiling_polyml-5.6.ML"
ab52f183f020 clarified directory structure;
wenzelm
parents: 61794
diff changeset
    26
    "RAW/ml_profiling_polyml.ML"
ab52f183f020 clarified directory structure;
wenzelm
parents: 61794
diff changeset
    27
    "RAW/ml_stack_dummy.ML"
ab52f183f020 clarified directory structure;
wenzelm
parents: 61794
diff changeset
    28
    "RAW/ml_stack_polyml-5.6.ML"
ab52f183f020 clarified directory structure;
wenzelm
parents: 61794
diff changeset
    29
    "RAW/ml_system.ML"
ab52f183f020 clarified directory structure;
wenzelm
parents: 61794
diff changeset
    30
    "RAW/multithreading.ML"
ab52f183f020 clarified directory structure;
wenzelm
parents: 61794
diff changeset
    31
    "RAW/single_assignment_polyml.ML"
ab52f183f020 clarified directory structure;
wenzelm
parents: 61794
diff changeset
    32
    "RAW/unsynchronized.ML"
48347
8bb27ab9e841 more explicit treatment of initial Pure sessions;
wenzelm
parents:
diff changeset
    33
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48732
diff changeset
    34
session Pure =
56801
8dd9df88f647 some support for session-qualified theories: allow to refer to resources via qualified name instead of odd file-system path;
wenzelm
parents: 56435
diff changeset
    35
  global_theories Pure
48514
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
    36
  files
62077
e8ae72c26025 clarified ROOT files;
wenzelm
parents: 61926
diff changeset
    37
    "RAW/ROOT_polyml-5.6.ML"
e8ae72c26025 clarified ROOT files;
wenzelm
parents: 61926
diff changeset
    38
    "RAW/ROOT_polyml.ML"
61925
ab52f183f020 clarified directory structure;
wenzelm
parents: 61794
diff changeset
    39
    "RAW/compiler_polyml.ML"
ab52f183f020 clarified directory structure;
wenzelm
parents: 61794
diff changeset
    40
    "RAW/exn.ML"
62459
7a5d88dd8cc9 support only polyml-5.3.0 and polyml-5.6;
wenzelm
parents: 62387
diff changeset
    41
    "RAW/exn_trace.ML"
62460
4b2018eb92e8 clarified;
wenzelm
parents: 62459
diff changeset
    42
    "RAW/exn_trace_raw.ML"
62387
ad3eb2889f9a support for polyml-git ec49a49972c5 (branch FixedPrecisionInt);
wenzelm
parents: 62359
diff changeset
    43
    "RAW/fixed_int_dummy.ML"
61925
ab52f183f020 clarified directory structure;
wenzelm
parents: 61794
diff changeset
    44
    "RAW/ml_compiler_parameters.ML"
ab52f183f020 clarified directory structure;
wenzelm
parents: 61794
diff changeset
    45
    "RAW/ml_compiler_parameters_polyml-5.6.ML"
ab52f183f020 clarified directory structure;
wenzelm
parents: 61794
diff changeset
    46
    "RAW/ml_debugger.ML"
ab52f183f020 clarified directory structure;
wenzelm
parents: 61794
diff changeset
    47
    "RAW/ml_debugger_polyml-5.6.ML"
62467
c1b88e647e2f clarified ML heap operations;
wenzelm
parents: 62460
diff changeset
    48
    "RAW/ml_heap.ML"
c1b88e647e2f clarified ML heap operations;
wenzelm
parents: 62460
diff changeset
    49
    "RAW/ml_heap_polyml-5.3.0.ML"
61925
ab52f183f020 clarified directory structure;
wenzelm
parents: 61794
diff changeset
    50
    "RAW/ml_name_space_polyml-5.6.ML"
ab52f183f020 clarified directory structure;
wenzelm
parents: 61794
diff changeset
    51
    "RAW/ml_name_space_polyml.ML"
ab52f183f020 clarified directory structure;
wenzelm
parents: 61794
diff changeset
    52
    "RAW/ml_parse_tree.ML"
ab52f183f020 clarified directory structure;
wenzelm
parents: 61794
diff changeset
    53
    "RAW/ml_parse_tree_polyml-5.6.ML"
ab52f183f020 clarified directory structure;
wenzelm
parents: 61794
diff changeset
    54
    "RAW/ml_positions.ML"
ab52f183f020 clarified directory structure;
wenzelm
parents: 61794
diff changeset
    55
    "RAW/ml_pretty.ML"
ab52f183f020 clarified directory structure;
wenzelm
parents: 61794
diff changeset
    56
    "RAW/ml_profiling_polyml-5.6.ML"
ab52f183f020 clarified directory structure;
wenzelm
parents: 61794
diff changeset
    57
    "RAW/ml_profiling_polyml.ML"
ab52f183f020 clarified directory structure;
wenzelm
parents: 61794
diff changeset
    58
    "RAW/ml_stack_dummy.ML"
ab52f183f020 clarified directory structure;
wenzelm
parents: 61794
diff changeset
    59
    "RAW/ml_stack_polyml-5.6.ML"
ab52f183f020 clarified directory structure;
wenzelm
parents: 61794
diff changeset
    60
    "RAW/ml_system.ML"
ab52f183f020 clarified directory structure;
wenzelm
parents: 61794
diff changeset
    61
    "RAW/multithreading.ML"
ab52f183f020 clarified directory structure;
wenzelm
parents: 61794
diff changeset
    62
    "RAW/single_assignment_polyml.ML"
ab52f183f020 clarified directory structure;
wenzelm
parents: 61794
diff changeset
    63
    "RAW/unsynchronized.ML"
48347
8bb27ab9e841 more explicit treatment of initial Pure sessions;
wenzelm
parents:
diff changeset
    64
48514
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
    65
    "Concurrent/bash.ML"
60962
faa452d8e265 basic setup for native Windows (RAW session without image);
wenzelm
parents: 60923
diff changeset
    66
    "Concurrent/bash_windows.ML"
48514
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
    67
    "Concurrent/cache.ML"
60908
d32915a03c63 more accurate dependencies;
wenzelm
parents: 60745
diff changeset
    68
    "Concurrent/counter.ML"
52050
b40ed9dcf903 event timer as separate service thread;
wenzelm
parents: 52010
diff changeset
    69
    "Concurrent/event_timer.ML"
48514
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
    70
    "Concurrent/future.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
    71
    "Concurrent/lazy.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
    72
    "Concurrent/mailbox.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
    73
    "Concurrent/par_exn.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
    74
    "Concurrent/par_list.ML"
59172
d1c500e0a722 separate module Random;
wenzelm
parents: 59064
diff changeset
    75
    "Concurrent/random.ML"
48514
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
    76
    "Concurrent/single_assignment.ML"
61556
0d4ee4168e41 clarified modules;
wenzelm
parents: 61441
diff changeset
    77
    "Concurrent/standard_thread.ML"
48514
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
    78
    "Concurrent/synchronized.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
    79
    "Concurrent/task_queue.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
    80
    "Concurrent/time_limit.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
    81
    "General/alist.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
    82
    "General/antiquote.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
    83
    "General/balanced_tree.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
    84
    "General/basics.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
    85
    "General/binding.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
    86
    "General/buffer.ML"
56053
030531cc4c62 tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
wenzelm
parents: 55672
diff changeset
    87
    "General/change_table.ML"
55672
5e25cc741ab9 support for completion within the formal context;
wenzelm
parents: 55516
diff changeset
    88
    "General/completion.ML"
48514
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
    89
    "General/file.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
    90
    "General/graph.ML"
49561
26fc70e983c2 separate module Graph_Display;
wenzelm
parents: 48916
diff changeset
    91
    "General/graph_display.ML"
48514
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
    92
    "General/heap.ML"
59064
a8bcb5a446c8 more abstract type Input.source;
wenzelm
parents: 59026
diff changeset
    93
    "General/input.ML"
48514
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
    94
    "General/integer.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
    95
    "General/linear_set.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
    96
    "General/long_name.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
    97
    "General/name_space.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
    98
    "General/ord_list.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
    99
    "General/output.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   100
    "General/path.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   101
    "General/position.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   102
    "General/pretty.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   103
    "General/print_mode.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   104
    "General/properties.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   105
    "General/queue.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   106
    "General/same.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   107
    "General/scan.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   108
    "General/secure.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   109
    "General/seq.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   110
    "General/sha1.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   111
    "General/sha1_polyml.ML"
53212
387b9f7cb0ac added SHA1 library integrity test, which is invoked at compile time and Isabelle_Process run-time;
wenzelm
parents: 52926
diff changeset
   112
    "General/sha1_samples.ML"
50800
c0fb2839d1a9 recovered buffered sockets from 11f622794ad6 -- requires Poly/ML 5.5.x;
wenzelm
parents: 50686
diff changeset
   113
    "General/socket_io.ML"
48514
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   114
    "General/source.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   115
    "General/stack.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   116
    "General/symbol.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   117
    "General/symbol_pos.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   118
    "General/table.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   119
    "General/timing.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   120
    "General/url.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   121
    "Isar/args.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   122
    "Isar/attrib.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   123
    "Isar/auto_bind.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   124
    "Isar/bundle.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   125
    "Isar/class.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   126
    "Isar/class_declaration.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   127
    "Isar/code.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   128
    "Isar/context_rules.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   129
    "Isar/element.ML"
59901
840d03805755 added command 'experiment';
wenzelm
parents: 59714
diff changeset
   130
    "Isar/experiment.ML"
48514
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   131
    "Isar/expression.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   132
    "Isar/generic_target.ML"
61677
a97232cf1981 leftover from 27ca6147e3b3
haftmann
parents: 61619
diff changeset
   133
    "Isar/interpretation.ML"
48514
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   134
    "Isar/isar_cmd.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   135
    "Isar/keyword.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   136
    "Isar/local_defs.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   137
    "Isar/local_theory.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   138
    "Isar/locale.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   139
    "Isar/method.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   140
    "Isar/named_target.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   141
    "Isar/object_logic.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   142
    "Isar/obtain.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   143
    "Isar/outer_syntax.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   144
    "Isar/overloading.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   145
    "Isar/parse.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   146
    "Isar/parse_spec.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   147
    "Isar/proof.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   148
    "Isar/proof_context.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   149
    "Isar/proof_display.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   150
    "Isar/proof_node.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   151
    "Isar/rule_cases.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   152
    "Isar/runtime.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   153
    "Isar/spec_rules.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   154
    "Isar/specification.ML"
60630
fc7625ec7427 clarified module;
wenzelm
parents: 59901
diff changeset
   155
    "Isar/subgoal.ML"
48514
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   156
    "Isar/token.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   157
    "Isar/toplevel.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   158
    "Isar/typedecl.ML"
62355
00f7618a9f2b clarified file names;
wenzelm
parents: 62354
diff changeset
   159
    "ML/exn_output.ML"
00f7618a9f2b clarified file names;
wenzelm
parents: 62354
diff changeset
   160
    "ML/exn_properties.ML"
48514
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   161
    "ML/install_pp_polyml.ML"
56072
31e427387ab5 tuned signature -- clarified module name;
wenzelm
parents: 56053
diff changeset
   162
    "ML/ml_antiquotation.ML"
62355
00f7618a9f2b clarified file names;
wenzelm
parents: 62354
diff changeset
   163
    "ML/ml_compiler.ML"
48514
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   164
    "ML/ml_context.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   165
    "ML/ml_env.ML"
58928
23d0ffd48006 plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents: 58846
diff changeset
   166
    "ML/ml_file.ML"
48514
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   167
    "ML/ml_lex.ML"
60908
d32915a03c63 more accurate dependencies;
wenzelm
parents: 60745
diff changeset
   168
    "ML/ml_options.ML"
48514
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   169
    "ML/ml_parse.ML"
62459
7a5d88dd8cc9 support only polyml-5.3.0 and polyml-5.6;
wenzelm
parents: 62387
diff changeset
   170
    "ML/ml_statistics.ML"
50255
d0ec1f0d1d7d some support for ML runtime statistics;
wenzelm
parents: 50217
diff changeset
   171
    "ML/ml_statistics_dummy.ML"
48514
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   172
    "ML/ml_syntax.ML"
50450
358b6020f8b6 generalized notion of active area, where sendback is just one application;
wenzelm
parents: 50255
diff changeset
   173
    "PIDE/active.ML"
48514
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   174
    "PIDE/command.ML"
57905
c0c5652e796e separate module Command_Span: mostly syntactic representation;
wenzelm
parents: 56801
diff changeset
   175
    "PIDE/command_span.ML"
48514
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   176
    "PIDE/document.ML"
52530
99dd8b4ef3fe explicit module Document_ID as source of globally unique identifiers across ML/Scala;
wenzelm
parents: 52211
diff changeset
   177
    "PIDE/document_id.ML"
52605
a2a805549c74 clarified module name;
wenzelm
parents: 52596
diff changeset
   178
    "PIDE/execution.ML"
48514
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   179
    "PIDE/markup.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   180
    "PIDE/protocol.ML"
59714
ae322325adbb tuned protocol -- resolve command positions in ML;
wenzelm
parents: 59470
diff changeset
   181
    "PIDE/protocol_message.ML"
52865
02a7e7180ee5 slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents: 52836
diff changeset
   182
    "PIDE/query_operation.ML"
56208
06cc31dff138 clarifed module name;
wenzelm
parents: 56072
diff changeset
   183
    "PIDE/resources.ML"
56210
c7c85cdb725d clarified module arrangement;
wenzelm
parents: 56208
diff changeset
   184
    "PIDE/session.ML"
48514
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   185
    "PIDE/xml.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   186
    "PIDE/yxml.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   187
    "Proof/extraction.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   188
    "Proof/proof_checker.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   189
    "Proof/proof_rewrite_rules.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   190
    "Proof/proof_syntax.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   191
    "Proof/reconstruct.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   192
    "ROOT.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   193
    "Syntax/ast.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   194
    "Syntax/lexicon.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   195
    "Syntax/local_syntax.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   196
    "Syntax/mixfix.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   197
    "Syntax/parser.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   198
    "Syntax/printer.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   199
    "Syntax/simple_syntax.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   200
    "Syntax/syntax.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   201
    "Syntax/syntax_ext.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   202
    "Syntax/syntax_phases.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   203
    "Syntax/syntax_trans.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   204
    "Syntax/term_position.ML"
52211
66bc827e37f8 explicit support for type annotations within printed syntax trees;
wenzelm
parents: 52050
diff changeset
   205
    "Syntax/type_annotation.ML"
48681
181b91e1d1c1 prefer general Command_Line.tool wrapper (cf. Scala version);
wenzelm
parents: 48646
diff changeset
   206
    "System/command_line.ML"
48514
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   207
    "System/invoke_scala.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   208
    "System/isabelle_process.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   209
    "System/isabelle_system.ML"
52584
5cad4a5f5615 more abstract message channel;
wenzelm
parents: 52530
diff changeset
   210
    "System/message_channel.ML"
48514
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   211
    "System/options.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   212
    "System/system_channel.ML"
61619
f22054b192b0 clarified modules;
wenzelm
parents: 61556
diff changeset
   213
    "Thy/document_antiquotations.ML"
48514
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   214
    "Thy/html.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   215
    "Thy/latex.ML"
61441
20ff1d5c74e1 minimal support for Markdown documents;
wenzelm
parents: 61268
diff changeset
   216
    "Thy/markdown.ML"
48514
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   217
    "Thy/present.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   218
    "Thy/term_style.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   219
    "Thy/thy_header.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   220
    "Thy/thy_info.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   221
    "Thy/thy_output.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   222
    "Thy/thy_syntax.ML"
50686
d703e3aafa8c moved files;
wenzelm
parents: 50450
diff changeset
   223
    "Tools/build.ML"
48514
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   224
    "Tools/named_thms.ML"
58660
8d4aebb9e327 clarified load order;
wenzelm
parents: 58470
diff changeset
   225
    "Tools/plugin.ML"
48514
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   226
    "assumption.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   227
    "axclass.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   228
    "config.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   229
    "conjunction.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   230
    "consts.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   231
    "context.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   232
    "context_position.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   233
    "conv.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   234
    "defs.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   235
    "drule.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   236
    "envir.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   237
    "facts.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   238
    "global_theory.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   239
    "goal.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   240
    "goal_display.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   241
    "item_net.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   242
    "library.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   243
    "logic.ML"
59026
30b8a5825a9c removed some add-ons from modules that are relevant for the inference kernel;
wenzelm
parents: 58928
diff changeset
   244
    "more_pattern.ML"
48514
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   245
    "more_thm.ML"
59026
30b8a5825a9c removed some add-ons from modules that are relevant for the inference kernel;
wenzelm
parents: 58928
diff changeset
   246
    "more_unify.ML"
48514
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   247
    "morphism.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   248
    "name.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   249
    "net.ML"
58009
987c848d509b clarified modules;
wenzelm
parents: 57934
diff changeset
   250
    "par_tactical.ML"
48514
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   251
    "pattern.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   252
    "primitive_defs.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   253
    "proofterm.ML"
48879
cb5cdbb645cd clarified bootstrapping of Pure;
wenzelm
parents: 48738
diff changeset
   254
    "pure_syn.ML"
48514
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   255
    "pure_thy.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   256
    "raw_simplifier.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   257
    "search.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   258
    "sign.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   259
    "simplifier.ML"
51551
88d1d19fb74f tuned signature and module arrangement;
wenzelm
parents: 51397
diff changeset
   260
    "skip_proof.ML"
48514
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   261
    "sorts.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   262
    "tactic.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   263
    "tactical.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   264
    "term.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   265
    "term_ord.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   266
    "term_sharing.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   267
    "term_subst.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   268
    "term_xml.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   269
    "theory.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   270
    "thm.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   271
    "type.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   272
    "type_infer.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   273
    "type_infer_context.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   274
    "unify.ML"
84df8858c8ac more files for session Pure;
wenzelm
parents: 48422
diff changeset
   275
    "variable.ML"