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