src/Pure/Thy/thy_info.ML
author wenzelm
Sat Mar 09 23:57:07 2019 +0100 (2 months ago ago)
changeset 70067 0cb8753bdb50
parent 70064 f8293bf510a0
child 70072 def3ec9cdb7e
permissions -rw-r--r--
clarified signature;
berghofe@3604
     1
(*  Title:      Pure/Thy/thy_info.ML
wenzelm@6211
     2
    Author:     Markus Wenzel, TU Muenchen
berghofe@3604
     3
wenzelm@37978
     4
Global theory info database, with auto-loading according to theory and
wenzelm@15801
     5
file dependencies.
wenzelm@3976
     6
*)
berghofe@3604
     7
berghofe@3604
     8
signature THY_INFO =
berghofe@3604
     9
sig
wenzelm@68181
    10
  type presentation_context =
wenzelm@68185
    11
    {options: Options.T, file_pos: Position.T, adjust_pos: Position.T -> Position.T,
wenzelm@68185
    12
      segments: Thy_Output.segment list}
wenzelm@68181
    13
  val apply_presentation: presentation_context -> theory -> unit
wenzelm@68181
    14
  val add_presentation: (presentation_context -> theory -> unit) -> theory -> theory
wenzelm@26614
    15
  val get_names: unit -> string list
wenzelm@7288
    16
  val lookup_theory: string -> theory option
wenzelm@6211
    17
  val get_theory: string -> theory
wenzelm@26983
    18
  val master_directory: string -> Path.T
wenzelm@29421
    19
  val remove_thy: string -> unit
wenzelm@68180
    20
  type context =
wenzelm@68180
    21
    {options: Options.T,
wenzelm@61381
    22
     symbols: HTML.symbols,
wenzelm@67297
    23
     bibtex_entries: string list,
wenzelm@68180
    24
     last_timing: Toplevel.transition -> Time.time}
wenzelm@68180
    25
  val use_theories: context -> string -> Path.T -> (string * Position.T) list -> unit
wenzelm@65444
    26
  val use_thy: string -> unit
wenzelm@58856
    27
  val script_thy: Position.T -> string -> theory -> theory
wenzelm@37954
    28
  val register_thy: theory -> unit
wenzelm@24080
    29
  val finish: unit -> unit
berghofe@3604
    30
end;
berghofe@3604
    31
wenzelm@37216
    32
structure Thy_Info: THY_INFO =
wenzelm@6211
    33
struct
berghofe@3604
    34
wenzelm@68153
    35
(** presentation of consolidated theory **)
wenzelm@68153
    36
wenzelm@68181
    37
type presentation_context =
wenzelm@68185
    38
  {options: Options.T, file_pos: Position.T, adjust_pos: Position.T -> Position.T,
wenzelm@68185
    39
    segments: Thy_Output.segment list};
wenzelm@68181
    40
wenzelm@68153
    41
structure Presentation = Theory_Data
wenzelm@68153
    42
(
wenzelm@68181
    43
  type T = ((presentation_context -> theory -> unit) * stamp) list;
wenzelm@68153
    44
  val empty = [];
wenzelm@68153
    45
  val extend = I;
wenzelm@68153
    46
  fun merge data : T = Library.merge (eq_snd op =) data;
wenzelm@68153
    47
);
wenzelm@68153
    48
wenzelm@68181
    49
fun apply_presentation (context: presentation_context) thy =
wenzelm@68181
    50
  ignore (Presentation.get thy |> Par_List.map (fn (f, _) => f context thy));
wenzelm@68181
    51
wenzelm@68153
    52
fun add_presentation f = Presentation.map (cons (f, stamp ()));
wenzelm@68153
    53
wenzelm@68181
    54
val _ =
wenzelm@68185
    55
  Theory.setup (add_presentation (fn {options, file_pos, segments, ...} => fn thy =>
wenzelm@68183
    56
    if exists (Toplevel.is_skipped_proof o #state) segments then ()
wenzelm@68181
    57
    else
wenzelm@68182
    58
      let
wenzelm@68506
    59
        val body = Thy_Output.present_thy options thy segments;
wenzelm@68182
    60
        val option = Present.document_option options;
wenzelm@68182
    61
      in
wenzelm@68182
    62
        if #disabled option then ()
wenzelm@68182
    63
        else
wenzelm@68182
    64
          let
wenzelm@68182
    65
            val latex = Latex.isabelle_body (Context.theory_name thy) body;
wenzelm@68185
    66
            val output = [Latex.output_text latex, Latex.output_positions file_pos latex];
wenzelm@68491
    67
            val _ =
wenzelm@68491
    68
              if Options.bool options "export_document"
wenzelm@69800
    69
              then Export.export thy (Path.explode "document.tex") output else ();
wenzelm@68182
    70
            val _ = if #enabled option then Present.theory_output thy output else ();
wenzelm@68182
    71
          in () end
wenzelm@68182
    72
      end));
wenzelm@68153
    73
wenzelm@68153
    74
wenzelm@68153
    75
wenzelm@6211
    76
(** thy database **)
wenzelm@6211
    77
wenzelm@6211
    78
(* messages *)
wenzelm@6211
    79
wenzelm@55797
    80
val show_path = space_implode " via " o map quote;
wenzelm@6211
    81
wenzelm@55797
    82
fun cycle_msg names = "Cyclic dependency of " ^ show_path names;
berghofe@3604
    83
berghofe@3604
    84
wenzelm@6666
    85
(* derived graph operations *)
berghofe@3604
    86
wenzelm@50862
    87
fun add_deps name parents G = String_Graph.add_deps_acyclic (name, parents) G
wenzelm@50862
    88
  handle String_Graph.CYCLES namess => error (cat_lines (map cycle_msg namess));
berghofe@3604
    89
wenzelm@37984
    90
fun new_entry name parents entry =
wenzelm@50862
    91
  String_Graph.new_node (name, entry) #> add_deps name parents;
wenzelm@37977
    92
berghofe@3604
    93
wenzelm@59178
    94
(* global thys *)
wenzelm@6211
    95
wenzelm@6211
    96
type deps =
wenzelm@41955
    97
 {master: (Path.T * SHA1.digest),  (*master dependencies for thy file*)
wenzelm@48927
    98
  imports: (string * Position.T) list};  (*source specification of imports (partially qualified)*)
wenzelm@23886
    99
wenzelm@38148
   100
fun make_deps master imports : deps = {master = master, imports = imports};
wenzelm@6211
   101
wenzelm@65454
   102
fun master_dir_deps (d: deps option) =
wenzelm@59178
   103
  the_default Path.current (Option.map (Path.dir o #1 o #master) d);
wenzelm@59178
   104
wenzelm@6211
   105
local
wenzelm@59178
   106
  val global_thys =
wenzelm@59178
   107
    Synchronized.var "Thy_Info.thys"
wenzelm@59178
   108
      (String_Graph.empty: (deps option * theory option) String_Graph.T);
wenzelm@6211
   109
in
wenzelm@59178
   110
  fun get_thys () = Synchronized.value global_thys;
wenzelm@59178
   111
  fun change_thys f = Synchronized.change global_thys f;
berghofe@3604
   112
end;
wenzelm@5209
   113
wenzelm@50862
   114
fun get_names () = String_Graph.topological_order (get_thys ());
wenzelm@6211
   115
wenzelm@6211
   116
wenzelm@6211
   117
(* access thy *)
wenzelm@6211
   118
wenzelm@59178
   119
fun lookup thys name = try (String_Graph.get_node thys) name;
wenzelm@59178
   120
fun lookup_thy name = lookup (get_thys ()) name;
wenzelm@7935
   121
wenzelm@59178
   122
fun get thys name =
wenzelm@59178
   123
  (case lookup thys name of
skalberg@15531
   124
    SOME thy => thy
wenzelm@55797
   125
  | NONE => error ("Theory loader: nothing known about theory " ^ quote name));
wenzelm@6211
   126
wenzelm@59178
   127
fun get_thy name = get (get_thys ()) name;
wenzelm@59178
   128
wenzelm@6211
   129
wenzelm@6211
   130
(* access deps *)
wenzelm@6211
   131
skalberg@15570
   132
val lookup_deps = Option.map #1 o lookup_thy;
wenzelm@6211
   133
wenzelm@65454
   134
val master_directory = master_dir_deps o #1 o get_thy;
wenzelm@7191
   135
wenzelm@6211
   136
wenzelm@6211
   137
(* access theory *)
wenzelm@6211
   138
wenzelm@7687
   139
fun lookup_theory name =
wenzelm@7687
   140
  (case lookup_thy name of
wenzelm@38142
   141
    SOME (_, SOME theory) => SOME theory
skalberg@15531
   142
  | _ => NONE);
wenzelm@7288
   143
wenzelm@6211
   144
fun get_theory name =
wenzelm@7288
   145
  (case lookup_theory name of
wenzelm@23871
   146
    SOME theory => theory
wenzelm@55797
   147
  | _ => error ("Theory loader: undefined entry for theory " ^ quote name));
wenzelm@6211
   148
wenzelm@56208
   149
val get_imports = Resources.imports_of o get_theory;
wenzelm@44337
   150
wenzelm@6211
   151
wenzelm@6211
   152
wenzelm@6211
   153
(** thy operations **)
wenzelm@6211
   154
wenzelm@59178
   155
(* remove *)
wenzelm@29421
   156
wenzelm@59178
   157
fun remove name thys =
wenzelm@59178
   158
  (case lookup thys name of
wenzelm@59178
   159
    NONE => thys
wenzelm@59178
   160
  | SOME (NONE, _) => error ("Cannot update finished theory " ^ quote name)
wenzelm@59178
   161
  | SOME _ =>
wenzelm@59178
   162
      let
wenzelm@59178
   163
        val succs = String_Graph.all_succs thys [name];
wenzelm@59178
   164
        val _ = writeln ("Theory loader: removing " ^ commas_quote succs);
wenzelm@59178
   165
      in fold String_Graph.del_node succs thys end);
wenzelm@29421
   166
wenzelm@59178
   167
val remove_thy = change_thys o remove;
wenzelm@59178
   168
wenzelm@7099
   169
wenzelm@59178
   170
(* update *)
wenzelm@59178
   171
wenzelm@59178
   172
fun update deps theory thys =
wenzelm@43640
   173
  let
wenzelm@65459
   174
    val name = Context.theory_long_name theory;
wenzelm@65459
   175
    val parents = map Context.theory_long_name (Theory.parents_of theory);
wenzelm@59178
   176
wenzelm@59178
   177
    val thys' = remove name thys;
wenzelm@59178
   178
    val _ = map (get thys') parents;
wenzelm@59178
   179
  in new_entry name parents (SOME deps, SOME theory) thys' end;
wenzelm@59178
   180
wenzelm@59178
   181
fun update_thy deps theory = change_thys (update deps theory);
wenzelm@43640
   182
wenzelm@7099
   183
wenzelm@68180
   184
(* context *)
wenzelm@68180
   185
wenzelm@68180
   186
type context =
wenzelm@68180
   187
  {options: Options.T,
wenzelm@68180
   188
   symbols: HTML.symbols,
wenzelm@68180
   189
   bibtex_entries: string list,
wenzelm@68180
   190
   last_timing: Toplevel.transition -> Time.time};
wenzelm@68180
   191
wenzelm@68180
   192
fun default_context (): context =
wenzelm@68180
   193
  {options = Options.default (),
wenzelm@68180
   194
   symbols = HTML.no_symbols,
wenzelm@68180
   195
   bibtex_entries = [],
wenzelm@68180
   196
   last_timing = K Time.zeroTime};
wenzelm@68180
   197
wenzelm@68180
   198
wenzelm@24209
   199
(* scheduling loader tasks *)
wenzelm@24209
   200
wenzelm@51330
   201
datatype result =
wenzelm@53375
   202
  Result of {theory: theory, exec_id: Document_ID.exec,
wenzelm@53375
   203
    present: unit -> unit, commit: unit -> unit, weight: int};
wenzelm@51331
   204
wenzelm@53375
   205
fun theory_result theory =
wenzelm@53375
   206
  Result {theory = theory, exec_id = Document_ID.none, present = I, commit = I, weight = 0};
wenzelm@51330
   207
wenzelm@51330
   208
fun result_theory (Result {theory, ...}) = theory;
wenzelm@51331
   209
fun result_present (Result {present, ...}) = present;
wenzelm@51331
   210
fun result_commit (Result {commit, ...}) = commit;
wenzelm@51331
   211
fun result_ord (Result {weight = i, ...}, Result {weight = j, ...}) = int_ord (j, i);
wenzelm@51331
   212
wenzelm@53375
   213
fun join_theory (Result {theory, exec_id, ...}) =
wenzelm@54370
   214
  let
wenzelm@66374
   215
    val _ = Execution.join [exec_id];
wenzelm@64574
   216
    val res = Exn.capture Thm.consolidate_theory theory;
wenzelm@66380
   217
    val exns = maps Task_Queue.group_status (Execution.peek exec_id);
wenzelm@66380
   218
  in res :: map Exn.Exn exns end;
wenzelm@43641
   219
wenzelm@37977
   220
datatype task =
wenzelm@66711
   221
  Task of string list * (theory list -> result) |
wenzelm@37977
   222
  Finished of theory;
wenzelm@37977
   223
wenzelm@37977
   224
fun task_finished (Task _) = false
wenzelm@37977
   225
  | task_finished (Finished _) = true;
wenzelm@24209
   226
wenzelm@44162
   227
fun task_parents deps (parents: string list) = map (the o AList.lookup (op =) deps) parents;
wenzelm@44162
   228
wenzelm@44162
   229
val schedule_seq =
wenzelm@50862
   230
  String_Graph.schedule (fn deps => fn (_, task) =>
wenzelm@44162
   231
    (case task of
wenzelm@66711
   232
      Task (parents, body) =>
wenzelm@51331
   233
        let
wenzelm@51331
   234
          val result = body (task_parents deps parents);
wenzelm@53190
   235
          val _ = Par_Exn.release_all (join_theory result);
wenzelm@51331
   236
          val _ = result_present result ();
wenzelm@51331
   237
          val _ = result_commit result ();
wenzelm@51331
   238
        in result_theory result end
wenzelm@44162
   239
    | Finished thy => thy)) #> ignore;
wenzelm@29000
   240
wenzelm@62923
   241
val schedule_futures = Thread_Attributes.uninterruptible (fn _ => fn tasks =>
wenzelm@51284
   242
  let
wenzelm@51331
   243
    val futures = tasks
wenzelm@51284
   244
      |> String_Graph.schedule (fn deps => fn (name, task) =>
wenzelm@51284
   245
        (case task of
wenzelm@66711
   246
          Task (parents, body) =>
wenzelm@51284
   247
            (singleton o Future.forks)
wenzelm@51284
   248
              {name = "theory:" ^ name, group = NONE,
wenzelm@51284
   249
                deps = map (Future.task_of o #2) deps, pri = 0, interrupts = true}
wenzelm@51284
   250
              (fn () =>
wenzelm@51284
   251
                (case filter (not o can Future.join o #2) deps of
wenzelm@51330
   252
                  [] => body (map (result_theory o Future.join) (task_parents deps parents))
wenzelm@51284
   253
                | bad =>
wenzelm@55797
   254
                    error
wenzelm@55797
   255
                      ("Failed to load theory " ^ quote name ^
wenzelm@55797
   256
                        " (unresolved " ^ commas_quote (map #1 bad) ^ ")")))
wenzelm@51331
   257
        | Finished theory => Future.value (theory_result theory)));
wenzelm@51331
   258
wenzelm@51331
   259
    val results1 = futures
wenzelm@51331
   260
      |> maps (fn future =>
wenzelm@51331
   261
          (case Future.join_result future of
wenzelm@53190
   262
            Exn.Res result => join_theory result
wenzelm@51331
   263
          | Exn.Exn exn => [Exn.Exn exn]));
wenzelm@51331
   264
wenzelm@51331
   265
    val results2 = futures
wenzelm@51331
   266
      |> map_filter (Exn.get_res o Future.join_result)
wenzelm@51331
   267
      |> sort result_ord
wenzelm@51331
   268
      |> Par_List.map (fn result => Exn.capture (result_present result) ());
wenzelm@51331
   269
wenzelm@51331
   270
    (* FIXME more precise commit order (!?) *)
wenzelm@51331
   271
    val results3 = futures
wenzelm@51331
   272
      |> map (fn future => Exn.capture (fn () => result_commit (Future.join future) ()) ());
wenzelm@51284
   273
wenzelm@54370
   274
    (* FIXME avoid global Execution.reset (!??) *)
wenzelm@53192
   275
    val results4 = map Exn.Exn (maps Task_Queue.group_status (Execution.reset ()));
wenzelm@51284
   276
wenzelm@51331
   277
    val _ = Par_Exn.release_all (results1 @ results2 @ results3 @ results4);
wenzelm@51284
   278
  in () end);
wenzelm@29429
   279
wenzelm@24209
   280
wenzelm@65505
   281
(* eval theory *)
wenzelm@65505
   282
wenzelm@65505
   283
fun excursion keywords master_dir last_timing init elements =
wenzelm@65505
   284
  let
wenzelm@65505
   285
    fun prepare_span st span =
wenzelm@65505
   286
      Command_Span.content span
wenzelm@65505
   287
      |> Command.read keywords (Command.read_thy st) master_dir init ([], ~1)
wenzelm@70058
   288
      |> (fn tr => Toplevel.timing (last_timing tr) tr);
wenzelm@65505
   289
wenzelm@65505
   290
    fun element_result span_elem (st, _) =
wenzelm@65505
   291
      let
wenzelm@68839
   292
        val elem = Thy_Element.map_element (prepare_span st) span_elem;
wenzelm@65505
   293
        val (results, st') = Toplevel.element_result keywords elem st;
wenzelm@68839
   294
        val pos' = Toplevel.pos_of (Thy_Element.last_element elem);
wenzelm@65505
   295
      in (results, (st', pos')) end;
wenzelm@65505
   296
wenzelm@65505
   297
    val (results, (end_state, end_pos)) =
wenzelm@70067
   298
      fold_map element_result elements (Toplevel.init_toplevel (), Position.none);
wenzelm@65505
   299
wenzelm@65505
   300
    val thy = Toplevel.end_theory end_pos end_state;
wenzelm@65505
   301
  in (results, thy) end;
wenzelm@65505
   302
wenzelm@68180
   303
fun eval_thy (context: context) update_time master_dir header text_pos text parents =
wenzelm@65505
   304
  let
wenzelm@68180
   305
    val {options, symbols, bibtex_entries, last_timing} = context;
wenzelm@65505
   306
    val (name, _) = #name header;
wenzelm@65505
   307
    val keywords =
wenzelm@65505
   308
      fold (curry Keyword.merge_keywords o Thy_Header.get_keywords) parents
wenzelm@65505
   309
        (Keyword.add_keywords (#keywords header) Keyword.empty_keywords);
wenzelm@65505
   310
wenzelm@68179
   311
    val spans = Outer_Syntax.parse_spans (Token.explode keywords text_pos text);
wenzelm@68839
   312
    val elements = Thy_Element.parse_elements keywords spans;
wenzelm@65505
   313
wenzelm@65505
   314
    fun init () =
wenzelm@65505
   315
      Resources.begin_theory master_dir header parents
wenzelm@67297
   316
      |> Present.begin_theory bibtex_entries update_time
wenzelm@65505
   317
        (fn () => implode (map (HTML.present_span symbols keywords) spans));
wenzelm@65505
   318
wenzelm@65505
   319
    val (results, thy) =
wenzelm@65505
   320
      cond_timeit true ("theory " ^ quote name)
wenzelm@65505
   321
        (fn () => excursion keywords master_dir last_timing init elements);
wenzelm@65505
   322
wenzelm@65505
   323
    fun present () =
wenzelm@65505
   324
      let
wenzelm@68179
   325
        val segments = (spans ~~ maps Toplevel.join_results results)
wenzelm@68183
   326
          |> map (fn (span, (tr, st')) => {span = span, command = tr, state = st'});
wenzelm@68185
   327
        val context: presentation_context =
wenzelm@68185
   328
          {options = options, file_pos = text_pos, adjust_pos = I, segments = segments};
wenzelm@68181
   329
      in apply_presentation context thy end;
wenzelm@65505
   330
  in (thy, present, size text) end;
wenzelm@65505
   331
wenzelm@65505
   332
wenzelm@23967
   333
(* require_thy -- checking database entries wrt. the file-system *)
berghofe@15065
   334
wenzelm@7211
   335
local
wenzelm@6211
   336
wenzelm@37977
   337
fun required_by _ [] = ""
wenzelm@37977
   338
  | required_by s initiators = s ^ "(required by " ^ show_path (rev initiators) ^ ")";
wenzelm@37977
   339
wenzelm@67297
   340
fun load_thy context initiators update_time deps text (name, pos) keywords parents =
wenzelm@37977
   341
  let
wenzelm@59178
   342
    val _ = remove_thy name;
wenzelm@58843
   343
    val _ = writeln ("Loading theory " ^ quote name ^ required_by " " initiators);
wenzelm@56333
   344
    val _ = Output.try_protocol_message (Markup.loading_theory name) [];
wenzelm@37977
   345
wenzelm@41548
   346
    val {master = (thy_path, _), imports} = deps;
wenzelm@38134
   347
    val dir = Path.dir thy_path;
wenzelm@51294
   348
    val header = Thy_Header.make (name, pos) imports keywords;
wenzelm@48927
   349
wenzelm@48927
   350
    val _ = Position.reports (map #2 imports ~~ map Theory.get_markup parents);
wenzelm@37977
   351
wenzelm@53375
   352
    val exec_id = Document_ID.make ();
wenzelm@53375
   353
    val _ =
wenzelm@53375
   354
      Execution.running Document_ID.none exec_id [] orelse
wenzelm@53375
   355
        raise Fail ("Failed to register execution: " ^ Document_ID.print exec_id);
wenzelm@53375
   356
wenzelm@66873
   357
    val timing_start = Timing.start ();
wenzelm@66873
   358
wenzelm@53375
   359
    val text_pos = Position.put_id (Document_ID.print exec_id) (Path.position thy_path);
wenzelm@51331
   360
    val (theory, present, weight) =
wenzelm@67297
   361
      eval_thy context update_time dir header text_pos text
wenzelm@62876
   362
        (if name = Context.PureN then [Context.the_global_context ()] else parents);
wenzelm@66873
   363
wenzelm@66873
   364
    val timing_result = Timing.result timing_start;
wenzelm@66873
   365
    val timing_props = [Markup.theory_timing, (Markup.nameN, name)];
wenzelm@66873
   366
    val _  = Output.try_protocol_message (timing_props @ Markup.timing_properties timing_result) []
wenzelm@66873
   367
wenzelm@43640
   368
    fun commit () = update_thy deps theory;
wenzelm@53375
   369
  in
wenzelm@53375
   370
    Result {theory = theory, exec_id = exec_id, present = present, commit = commit, weight = weight}
wenzelm@53375
   371
  end;
wenzelm@37977
   372
wenzelm@48898
   373
fun check_deps dir name =
wenzelm@6211
   374
  (case lookup_deps name of
wenzelm@51293
   375
    SOME NONE => (true, NONE, Position.none, get_imports name, [])
wenzelm@23893
   376
  | NONE =>
wenzelm@56208
   377
      let val {master, text, theory_pos, imports, keywords} = Resources.check_thy dir name
wenzelm@51293
   378
      in (false, SOME (make_deps master imports, text), theory_pos, imports, keywords) end
wenzelm@42129
   379
  | SOME (SOME {master, ...}) =>
wenzelm@42003
   380
      let
wenzelm@48928
   381
        val {master = master', text = text', theory_pos = theory_pos', imports = imports',
wenzelm@56208
   382
          keywords = keywords'} = Resources.check_thy dir name;
wenzelm@42003
   383
        val deps' = SOME (make_deps master' imports', text');
wenzelm@42003
   384
        val current =
wenzelm@42003
   385
          #2 master = #2 master' andalso
wenzelm@42003
   386
            (case lookup_theory name of
wenzelm@42003
   387
              NONE => false
wenzelm@56208
   388
            | SOME theory => Resources.loaded_files_current theory);
wenzelm@51293
   389
      in (current, deps', theory_pos', imports', keywords') end);
wenzelm@6211
   390
wenzelm@23967
   391
in
wenzelm@23967
   392
wenzelm@67297
   393
fun require_thys context initiators qualifier dir strs tasks =
wenzelm@67297
   394
      fold_map (require_thy context initiators qualifier dir) strs tasks |>> forall I
wenzelm@67297
   395
and require_thy context initiators qualifier dir (s, require_pos) tasks =
wenzelm@6211
   396
  let
wenzelm@66711
   397
    val {master_dir, theory_name, ...} = Resources.import_name qualifier dir s;
wenzelm@7066
   398
  in
wenzelm@65443
   399
    (case try (String_Graph.get_node tasks) theory_name of
wenzelm@66711
   400
      SOME task => (task_finished task, tasks)
wenzelm@23967
   401
    | NONE =>
wenzelm@23967
   402
        let
wenzelm@65443
   403
          val _ = member (op =) initiators theory_name andalso error (cycle_msg initiators);
wenzelm@43651
   404
wenzelm@65454
   405
          val (current, deps, theory_pos, imports, keywords) = check_deps master_dir theory_name
wenzelm@55797
   406
            handle ERROR msg =>
wenzelm@55797
   407
              cat_error msg
wenzelm@65443
   408
                ("The error(s) above occurred for theory " ^ quote theory_name ^
wenzelm@55797
   409
                  Position.here require_pos ^ required_by "\n" initiators);
wenzelm@37981
   410
wenzelm@65455
   411
          val qualifier' = Resources.theory_qualifier theory_name;
wenzelm@65455
   412
          val dir' = Path.append dir (master_dir_deps (Option.map #1 deps));
wenzelm@65455
   413
wenzelm@65455
   414
          val parents = map (#theory_name o Resources.import_name qualifier' dir' o #1) imports;
wenzelm@48898
   415
          val (parents_current, tasks') =
wenzelm@67297
   416
            require_thys context (theory_name :: initiators) qualifier' dir' imports tasks;
wenzelm@6211
   417
wenzelm@23967
   418
          val all_current = current andalso parents_current;
wenzelm@37977
   419
          val task =
wenzelm@65443
   420
            if all_current then Finished (get_theory theory_name)
wenzelm@37977
   421
            else
wenzelm@37980
   422
              (case deps of
wenzelm@37980
   423
                NONE => raise Fail "Malformed deps"
wenzelm@42003
   424
              | SOME (dep, text) =>
wenzelm@48876
   425
                  let
wenzelm@48876
   426
                    val update_time = serial ();
wenzelm@48928
   427
                    val load =
wenzelm@67297
   428
                      load_thy context initiators update_time
wenzelm@67297
   429
                        dep text (theory_name, theory_pos) keywords;
wenzelm@66711
   430
                  in Task (parents, load) end);
wenzelm@48874
   431
wenzelm@65443
   432
          val tasks'' = new_entry theory_name parents task tasks';
wenzelm@48898
   433
        in (all_current, tasks'') end)
wenzelm@7066
   434
  end;
wenzelm@6484
   435
wenzelm@23967
   436
end;
wenzelm@23967
   437
wenzelm@23967
   438
wenzelm@65444
   439
(* use theories *)
wenzelm@23967
   440
wenzelm@68180
   441
fun use_theories context qualifier master_dir imports =
wenzelm@68180
   442
  let val (_, tasks) = require_thys context [] qualifier master_dir imports String_Graph.empty
wenzelm@68132
   443
  in if Multithreading.max_threads () > 1 then schedule_futures tasks else schedule_seq tasks end;
wenzelm@23967
   444
wenzelm@65444
   445
fun use_thy name =
wenzelm@68180
   446
  use_theories (default_context ()) Resources.default_qualifier
wenzelm@68180
   447
    Path.current [(name, Position.none)];
wenzelm@7211
   448
wenzelm@59364
   449
wenzelm@57626
   450
(* toplevel scripting -- without maintaining database *)
wenzelm@57626
   451
wenzelm@58856
   452
fun script_thy pos txt thy =
wenzelm@57626
   453
  let
wenzelm@58856
   454
    val trs =
wenzelm@58928
   455
      Outer_Syntax.parse thy pos txt
wenzelm@58856
   456
      |> map (Toplevel.modify_init (K thy));
wenzelm@57626
   457
    val end_pos = if null trs then pos else Toplevel.pos_of (List.last trs);
wenzelm@70067
   458
    val end_state = fold (Toplevel.command_exception true) trs (Toplevel.init_toplevel ());
wenzelm@57626
   459
  in Toplevel.end_theory end_pos end_state end;
wenzelm@6211
   460
wenzelm@6211
   461
wenzelm@37977
   462
(* register theory *)
wenzelm@6211
   463
wenzelm@37954
   464
fun register_thy theory =
wenzelm@6211
   465
  let
wenzelm@65459
   466
    val name = Context.theory_long_name theory;
wenzelm@56208
   467
    val {master, ...} = Resources.check_thy (Resources.master_directory theory) name;
wenzelm@56208
   468
    val imports = Resources.imports_of theory;
wenzelm@6211
   469
  in
wenzelm@59178
   470
    change_thys (fn thys =>
wenzelm@59178
   471
      let
wenzelm@59178
   472
        val thys' = remove name thys;
wenzelm@59178
   473
        val _ = writeln ("Registering theory " ^ quote name);
wenzelm@59178
   474
      in update (make_deps master imports) theory thys' end)
wenzelm@6211
   475
  end;
wenzelm@6211
   476
wenzelm@24080
   477
wenzelm@24080
   478
(* finish all theories *)
wenzelm@24080
   479
wenzelm@50862
   480
fun finish () = change_thys (String_Graph.map (fn _ => fn (_, entry) => (NONE, entry)));
wenzelm@24080
   481
wenzelm@6211
   482
end;
wenzelm@62847
   483
wenzelm@65444
   484
fun use_thy name = Runtime.toplevel_program (fn () => Thy_Info.use_thy name);