added theorems;
authorwenzelm
Wed Sep 01 21:06:57 1999 +0200 (1999-09-01)
changeset 7409f8ce7b832598
parent 7408 1ec1567c1307
child 7410 7369a35fb3c2
added theorems;
improved files;
src/Pure/Thy/browser_info.ML
     1.1 --- a/src/Pure/Thy/browser_info.ML	Wed Sep 01 21:06:27 1999 +0200
     1.2 +++ b/src/Pure/Thy/browser_info.ML	Wed Sep 01 21:06:57 1999 +0200
     1.3 @@ -19,6 +19,7 @@
     1.4    val begin_theory: string -> string list -> (Path.T * bool) list -> theory -> theory
     1.5    val end_theory: string -> unit
     1.6    val theorem: string -> thm -> unit
     1.7 +  val theorems: string -> thm list -> unit
     1.8    val setup: (theory -> theory) list
     1.9  end;
    1.10  
    1.11 @@ -319,8 +320,8 @@
    1.12    let
    1.13      val parents = map (parent_link remote_path path) raw_parents;
    1.14      val ml_path = ThyLoad.ml_path name;
    1.15 -    val files = orig_files @		(* FIXME improve!? *)
    1.16 -      (if is_some (ThyLoad.check_file ml_path) then [(ml_path, true)] else []);
    1.17 +    val files = map (apsnd Some) orig_files @
    1.18 +      (if is_some (ThyLoad.check_file ml_path) then [(ml_path, None)] else []);
    1.19  
    1.20      fun prep_file (raw_path, loadit) =
    1.21        (case ThyLoad.check_file raw_path of
    1.22 @@ -359,6 +360,7 @@
    1.23  fun end_theory _ = ();
    1.24  
    1.25  fun theorem name thm = with_session () (fn _ => with_context add_html (HTML.theorem name thm));
    1.26 +fun theorems name thms = with_session () (fn _ => with_context add_html (HTML.theorems name thms));
    1.27  fun section s = with_session () (fn _ => with_context add_html (HTML.section s));
    1.28  
    1.29