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