simplified ThyLoad interfaces: only one additional directory;
authorwenzelm
Fri Jul 20 17:54:15 2007 +0200 (2007-07-20)
changeset 238841d39ec4fe73f
parent 23883 7d5aa704454e
child 23885 09254a1622e3
simplified ThyLoad interfaces: only one additional directory;
src/Pure/Isar/outer_syntax.ML
src/Pure/ProofGeneral/pgip_isabelle.ML
src/Pure/ProofGeneral/proof_general_pgip.ML
src/Pure/Thy/present.ML
     1.1 --- a/src/Pure/Isar/outer_syntax.ML	Fri Jul 20 15:29:25 2007 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.ML	Fri Jul 20 17:54:15 2007 +0200
     1.3 @@ -245,9 +245,9 @@
     1.4  
     1.5  local
     1.6  
     1.7 -fun try_ml_file dirs name time =
     1.8 +fun try_ml_file dir name time =
     1.9    let val path = ThyLoad.ml_path name in
    1.10 -    if is_none (ThyLoad.check_file dirs path) then ()
    1.11 +    if is_none (ThyLoad.check_file dir path) then ()
    1.12      else
    1.13        let
    1.14          val _ = legacy_feature ("loading attached ML script " ^ quote (Path.implode path));
    1.15 @@ -256,9 +256,9 @@
    1.16        in Toplevel.excursion [Toplevel.empty |> Toplevel.name tr_name |> tr] end
    1.17    end;
    1.18  
    1.19 -fun run_thy dirs name time =
    1.20 +fun run_thy dir name time =
    1.21    let
    1.22 -    val master as ((path, _), _) = ThyLoad.check_thy dirs name false;
    1.23 +    val master as ((path, _), _) = ThyLoad.check_thy dir name false;
    1.24      val text = Source.of_list (Library.untabify (explode (File.read path)));
    1.25  
    1.26      val _ = Present.init_theory name;
    1.27 @@ -280,11 +280,11 @@
    1.28  
    1.29    in master end;
    1.30  
    1.31 -fun load_thy dirs name ml time =
    1.32 +fun load_thy dir name ml time =
    1.33    let
    1.34 -    val master = run_thy dirs name time;
    1.35 +    val master = run_thy dir name time;
    1.36      val _ = ML_Context.set_context (SOME (Context.Theory (ThyInfo.get_theory name)));
    1.37 -    val _ = if ml then try_ml_file dirs name time else ();
    1.38 +    val _ = if ml then try_ml_file dir name time else ();
    1.39    in master end;
    1.40  
    1.41  in
     2.1 --- a/src/Pure/ProofGeneral/pgip_isabelle.ML	Fri Jul 20 15:29:25 2007 +0200
     2.2 +++ b/src/Pure/ProofGeneral/pgip_isabelle.ML	Fri Jul 20 17:54:15 2007 +0200
     2.3 @@ -80,7 +80,7 @@
     2.4                 NONE => (NONE, NONE)
     2.5               | SOME fname =>
     2.6                 let val path = Path.explode fname in
     2.7 -                 case ThyLoad.check_file [] path of
     2.8 +                 case ThyLoad.check_file Path.current path of
     2.9                     SOME _ => (SOME (PgipTypes.pgipurl_of_path path), NONE)
    2.10                   | NONE => (NONE, SOME fname)
    2.11                 end);
     3.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Fri Jul 20 15:29:25 2007 +0200
     3.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Fri Jul 20 17:54:15 2007 +0200
     3.3 @@ -692,14 +692,14 @@
     3.4  
     3.5          fun filerefs f =
     3.6              let val thy = thy_name f
     3.7 -                val (_, (_,filerefs)) = ThyLoad.deps_thy [Path.dir f] thy true
     3.8 +                val (_, (_,filerefs)) = ThyLoad.deps_thy (Path.dir f) thy true
     3.9              in
    3.10                  issue_pgip (Setrefs {url=url, thyname=NONE, objtype=SOME PgipTypes.ObjFile,
    3.11                                       name=NONE, idtables=[], fileurls=filerefs})
    3.12              end
    3.13  
    3.14          fun thyrefs thy =
    3.15 -            let val (_, (thyrefs,_)) = ThyLoad.deps_thy [] thy true
    3.16 +            let val (_, (thyrefs,_)) = ThyLoad.deps_thy Path.current thy true
    3.17              in
    3.18                  issue_pgip (Setrefs {url=url, thyname=thyname, objtype=SOME PgipTypes.ObjTheory,
    3.19                                       name=NONE, idtables=[{context=NONE, objtype=PgipTypes.ObjTheory,
     4.1 --- a/src/Pure/Thy/present.ML	Fri Jul 20 15:29:25 2007 +0200
     4.2 +++ b/src/Pure/Thy/present.ML	Fri Jul 20 17:54:15 2007 +0200
     4.3 @@ -25,8 +25,7 @@
     4.4    val init_theory: string -> unit
     4.5    val verbatim_source: string -> (unit -> Symbol.symbol list) -> unit
     4.6    val theory_output: string -> string -> unit
     4.7 -  val begin_theory: Path.T list -> string -> string list ->
     4.8 -    (Path.T * bool) list -> theory -> theory
     4.9 +  val begin_theory: Path.T -> string -> string list -> (Path.T * bool) list -> theory -> theory
    4.10    val add_hook: (string -> (string * thm list) list -> unit) -> unit
    4.11    val results: string -> (string * thm list) list -> unit
    4.12    val theorem: string -> thm -> unit
    4.13 @@ -452,16 +451,16 @@
    4.14         (html_path name))), name)
    4.15    end;
    4.16  
    4.17 -fun begin_theory dirs name raw_parents orig_files thy =
    4.18 +fun begin_theory dir name raw_parents orig_files thy =
    4.19      with_session thy (fn {name = sess_name, session, path, html_prefix, remote_path, ...} =>
    4.20    let
    4.21      val parents = map (parent_link remote_path path) raw_parents;
    4.22      val ml_path = ThyLoad.ml_path name;
    4.23      val files = map (apsnd SOME) orig_files @
    4.24 -      (if is_some (ThyLoad.check_file dirs ml_path) then [(ml_path, NONE)] else []);
    4.25 +      (if is_some (ThyLoad.check_file dir ml_path) then [(ml_path, NONE)] else []);
    4.26  
    4.27      fun prep_file (raw_path, loadit) =
    4.28 -      (case ThyLoad.check_ml dirs raw_path of
    4.29 +      (case ThyLoad.check_ml dir raw_path of
    4.30          SOME (path, _) =>
    4.31            let
    4.32              val base = Path.base path;
    4.33 @@ -471,8 +470,9 @@
    4.34                HTML.ml_file (Url.File base) (File.read path));
    4.35              (SOME (Url.File base_html), Url.File raw_path, loadit)
    4.36            end
    4.37 -      | NONE => (warning ("Browser info: expected to find ML file" ^ quote (Path.implode raw_path));
    4.38 -          (NONE, Url.File raw_path, loadit)));
    4.39 +      | NONE =>
    4.40 +          (warning ("Browser info: expected to find ML file" ^ quote (Path.implode raw_path));
    4.41 +            (NONE, Url.File raw_path, loadit)));
    4.42  
    4.43      val files_html = map prep_file files;
    4.44