src/Pure/Thy/present.ML
author wenzelm
Sun Jul 23 12:10:11 2000 +0200 (2000-07-23)
changeset 9416 9144976964e7
parent 9136 8196955b02ec
child 9452 fc02c5bacaab
permissions -rw-r--r--
removed all_sessions.graph;
improved graph 'directories';
tuned;
     1 (*  Title:      Pure/Thy/present.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel and Stefan Berghofer, TU Muenchen
     4     License:    GPL (GNU GENERAL PUBLIC LICENSE)
     5 
     6 Theory presentation: HTML, graph files, (PDF)LaTeX documents.
     7 *)
     8 
     9 signature BASIC_PRESENT =
    10 sig
    11   val section: string -> unit
    12 end;
    13 
    14 signature PRESENT =
    15 sig
    16   include BASIC_PRESENT
    17   val init: bool -> string -> string list -> string -> Path.T option -> Url.T option * bool -> unit
    18   val finish: unit -> unit
    19   val init_theory: string -> unit
    20   val verbatim_source: string -> (unit -> Symbol.symbol list) -> unit
    21   val old_symbol_source: string -> (unit -> Symbol.symbol list) -> unit
    22   val theory_output: string -> string -> unit
    23   val begin_theory: string -> string list -> (Path.T * bool) list -> theory -> theory
    24   val result: string -> string -> thm -> unit
    25   val results: string -> string -> thm list -> unit
    26   val theorem: string -> thm -> unit
    27   val theorems: string -> thm list -> unit
    28   val chapter: string -> unit
    29   val subsection: string -> unit
    30   val subsubsection: string -> unit
    31   val setup: (theory -> theory) list
    32   val get_info: theory -> {name: string, session: string list, is_local: bool}
    33 end;
    34 
    35 structure Present: PRESENT =
    36 struct
    37 
    38 
    39 (** paths **)
    40 
    41 val output_path = Path.variable "ISABELLE_BROWSER_INFO";
    42 
    43 val tex_ext = Path.ext "tex";
    44 val tex_path = tex_ext o Path.basic;
    45 val html_ext = Path.ext "html";
    46 val html_path = html_ext o Path.basic;
    47 val graph_path = Path.ext "graph" o Path.basic;
    48 val index_path = Path.basic "index.html";
    49 val doc_path = Path.basic "document";
    50 val doc_indexN = "session";
    51 
    52 val session_path = Path.basic ".session";
    53 val session_entries_path = Path.unpack ".session/entries";
    54 val pre_index_path = Path.unpack ".session/pre-index";
    55 
    56 fun mk_rel_path [] ys = Path.make ys
    57   | mk_rel_path xs [] = Path.appends (replicate (length xs) Path.parent)
    58   | mk_rel_path (ps as x :: xs) (qs as y :: ys) = if x = y then mk_rel_path xs ys else
    59       Path.appends (replicate (length ps) Path.parent @ [Path.make qs]);
    60 
    61 
    62 (** additional theory data **)
    63 
    64 structure BrowserInfoArgs =
    65 struct
    66   val name = "Pure/browser_info";
    67   type T = {name: string, session: string list, is_local: bool};
    68 
    69   val empty = {name = "Pure", session = [], is_local = false};
    70   val copy = I;
    71   fun prep_ext _ = empty;
    72   fun merge _ = empty;
    73   fun print _ _ = ();
    74 end;
    75 
    76 structure BrowserInfoData = TheoryDataFun(BrowserInfoArgs);
    77 
    78 fun get_info thy =
    79   if Theory.eq_thy (thy, ProtoPure.thy) then BrowserInfoArgs.empty
    80   else BrowserInfoData.get thy;
    81 
    82 
    83 
    84 (** graphs **)
    85 
    86 type graph_node =
    87   {name: string, ID: string, dir: string, unfold: bool,
    88    path: string, parents: string list};
    89 
    90 fun write_graph gr path =
    91   File.write path (cat_lines (map (fn {name, ID, dir, unfold, path, parents} =>
    92     "\"" ^ name ^ "\" \"" ^ ID ^ "\" \"" ^ dir ^ (if unfold then "\" + \"" else "\" \"") ^
    93     path ^ "\" > " ^ space_implode " " (map quote parents) ^ " ;") gr));
    94 
    95 fun ID_of sess s = space_implode "/" (sess @ [s]);
    96 
    97 (*retrieve graph data from initial theory loader database*)
    98 fun init_graph remote_path curr_sess = map (fn name =>
    99   let
   100     val {name = sess_name, session, is_local} = get_info (ThyInfo.theory name);
   101     val path' = Path.append (Path.make session) (html_path name);
   102   in
   103    {name = name, ID = ID_of session name, dir = sess_name,
   104     path =
   105       if null session then "" else
   106       if is_some remote_path andalso not is_local then
   107         Url.pack (Url.append (the remote_path) (Url.file
   108           (Path.append (Path.make session) (html_path name))))
   109       else Path.pack (Path.append (mk_rel_path curr_sess session) (html_path name)),
   110     unfold = false,
   111     parents =
   112       map (fn s => ID_of (#session (get_info (ThyInfo.theory s))) s) (ThyInfo.get_preds name)}
   113   end) (ThyInfo.names ());
   114 
   115 fun ins_graph_entry (entry as {ID, ...}) (gr: graph_node list) =
   116   filter_out (fn entry' => #ID entry' = ID) gr @ [entry];
   117 
   118 
   119 
   120 (** global browser info state **)
   121 
   122 (* type theory_info *)
   123 
   124 type theory_info = {tex_source: Buffer.T, html_source: Buffer.T, html: Buffer.T};
   125 
   126 fun make_theory_info (tex_source, html_source, html) =
   127   {tex_source = tex_source, html_source = html_source, html = html}: theory_info;
   128 
   129 val empty_theory_info = make_theory_info (Buffer.empty, Buffer.empty, Buffer.empty);
   130 
   131 fun map_theory_info f {tex_source, html_source, html} =
   132   make_theory_info (f (tex_source, html_source, html));
   133 
   134 
   135 (* type browser_info *)
   136 
   137 type browser_info = {theories: theory_info Symtab.table, tex_index: Buffer.T,
   138   html_index: Buffer.T, graph: graph_node list};
   139 
   140 fun make_browser_info (theories, tex_index, html_index, graph) =
   141   {theories = theories, tex_index = tex_index, html_index = html_index,
   142     graph = graph}: browser_info;
   143 
   144 val empty_browser_info = make_browser_info (Symtab.empty, Buffer.empty, Buffer.empty, []);
   145 
   146 fun init_browser_info remote_path curr_sess = make_browser_info
   147   (Symtab.empty, Buffer.empty, Buffer.empty, init_graph remote_path curr_sess);
   148 
   149 fun map_browser_info f {theories, tex_index, html_index, graph} =
   150   make_browser_info (f (theories, tex_index, html_index, graph));
   151 
   152 
   153 (* state *)
   154 
   155 val browser_info = ref empty_browser_info;
   156 
   157 fun change_browser_info f = browser_info := map_browser_info f (! browser_info);
   158 
   159 fun init_theory_info name info =
   160   change_browser_info (fn (theories, tex_index, html_index, graph) =>
   161     (Symtab.update ((name, info), theories), tex_index, html_index, graph));
   162 
   163 fun change_theory_info name f =
   164   change_browser_info (fn (info as (theories, tex_index, html_index, graph)) =>
   165     (case Symtab.lookup (theories, name) of
   166       None => (warning ("Browser info: cannot access theory document " ^ quote name); info)
   167     | Some info => (Symtab.update ((name, map_theory_info f info), theories),
   168         tex_index, html_index, graph)));
   169 
   170 
   171 fun add_tex_index txt =
   172   change_browser_info (fn (theories, tex_index, html_index, graph) =>
   173     (theories, Buffer.add txt tex_index, html_index, graph));
   174 
   175 fun add_html_index txt =
   176   change_browser_info (fn (theories, tex_index, html_index, graph) =>
   177     (theories, tex_index, Buffer.add txt html_index, graph));
   178 
   179 fun add_graph_entry e =
   180   change_browser_info (fn (theories, tex_index, html_index, graph) =>
   181     (theories, tex_index, html_index, ins_graph_entry e graph));
   182 
   183 fun add_tex_source name txt = change_theory_info name (fn (tex_source, html_source, html) =>
   184   (Buffer.add txt tex_source, html_source, html));
   185 
   186 fun add_html_source name txt = change_theory_info name (fn (tex_source, html_source, html) =>
   187   (tex_source, Buffer.add txt html_source, html));
   188 
   189 fun add_html name txt = change_theory_info name (fn (tex_source, html_source, html) =>
   190   (tex_source, html_source, Buffer.add txt html));
   191 
   192 
   193 
   194 (** global session state **)
   195 
   196 (* session_info *)
   197 
   198 type session_info =
   199   {name: string, parent: string, session: string, path: string list, html_prefix: Path.T,
   200     doc_format: string, doc_prefixes: (Path.T * Path.T option) option, remote_path: Url.T option};
   201 
   202 fun make_session_info
   203     (name, parent, session, path, html_prefix, doc_format, doc_prefixes, remote_path) =
   204   {name = name, parent = parent, session = session, path = path, html_prefix = html_prefix,
   205     doc_format = doc_format, doc_prefixes = doc_prefixes, remote_path = remote_path}: session_info;
   206 
   207 
   208 (* state *)
   209 
   210 val session_info = ref (None: session_info option);
   211 
   212 fun with_session x f = (case ! session_info of None => x | Some info => f info);
   213 fun with_context f = f (PureThy.get_name (Context.the_context ()));
   214 
   215 
   216 
   217 (** HTML output **)
   218 
   219 (* maintain index *)
   220 
   221 val session_entries =
   222   HTML.session_entries o
   223     map (fn name => (Url.file (Path.append (Path.basic name) index_path), name));
   224 
   225 fun get_entries dir =
   226   split_lines (File.read (Path.append dir session_entries_path));
   227 
   228 fun put_entries entries dir =
   229   File.write (Path.append dir session_entries_path) (cat_lines entries);
   230 
   231 
   232 fun create_index dir =
   233   File.read (Path.append dir pre_index_path) ^
   234     session_entries (get_entries dir) ^ HTML.end_index
   235   |> File.write (Path.append dir index_path);
   236 
   237 fun update_index dir name =
   238   (case try get_entries dir of
   239     None => warning ("Browser info: cannot access session index of " ^ quote (Path.pack dir))
   240   | Some es => (put_entries ((es \ name) @ [name]) dir; create_index dir));
   241 
   242 
   243 (* init session *)
   244 
   245 fun name_of_session elems = space_implode "/" ("Isabelle" :: elems);
   246 
   247 fun could_copy inpath outpath =
   248   if File.exists inpath then (File.copy inpath outpath; true)
   249   else false;
   250 
   251 fun copy_files path1 path2 =
   252   (File.mkdir path2;
   253    File.system_command
   254      ("cp " ^ File.sysify_path path1 ^ " " ^ File.sysify_path path2));
   255 
   256 
   257 fun init false _ _ _ _ _ = (browser_info := empty_browser_info; session_info := None)
   258   | init true doc path name dump_path (remote_path, first_time) =
   259       let
   260         val parent_name = name_of_session (Library.take (length path - 1, path));
   261         val session_name = name_of_session path;
   262         val sess_prefix = Path.make path;
   263 
   264         val out_path = Path.expand output_path;
   265         val html_prefix = Path.append out_path sess_prefix;
   266 
   267         val (doc_prefixes, document_path) =
   268           if doc = "" then (None, None)
   269           else (Some (Path.append html_prefix doc_path, dump_path), Some (Path.ext doc doc_path));
   270 
   271         val graph_up_lnk = (Url.file index_path, session_name);
   272 
   273         val _ =
   274           (copy_files (Path.unpack "~~/lib/browser/awtUtilities/*.class")
   275              (Path.append html_prefix (Path.basic "awtUtilities"));
   276            copy_files (Path.unpack "~~/lib/browser/GraphBrowser/*.class")
   277              (Path.append html_prefix (Path.basic "GraphBrowser")));
   278 
   279         fun prep_readme readme =
   280           let val readme_path = Path.basic readme in
   281             if could_copy readme_path (Path.append html_prefix readme_path) then Some readme_path
   282             else None
   283           end;
   284         val opt_readme =
   285           (case prep_readme "README.html" of None => prep_readme "README" | some => some);
   286 
   287         val parent_index_path = Path.append Path.parent index_path;
   288         val index_up_lnk = if first_time then
   289             Url.append (the remote_path) (Url.file (Path.append sess_prefix parent_index_path))
   290           else Url.file parent_index_path;
   291 
   292         val index_text = HTML.begin_index (index_up_lnk, parent_name)
   293           (Url.file index_path, session_name) (apsome Url.file opt_readme)
   294             (apsome Url.file document_path) (Url.unpack "medium.html");
   295       in
   296         File.mkdir (Path.append html_prefix session_path);
   297         File.write (Path.append html_prefix session_entries_path) "";
   298         if is_some doc_prefixes then File.copy_all doc_path html_prefix else ();
   299         seq (fn (name, txt) => File.write (Path.append html_prefix (Path.basic name)) txt)
   300           (HTML.applet_pages session_name graph_up_lnk);
   301         session_info := Some (make_session_info (name, parent_name, session_name, path,
   302           html_prefix, doc, doc_prefixes, remote_path));
   303         browser_info := init_browser_info remote_path path;
   304         add_html_index index_text
   305       end;
   306 
   307 
   308 (* finish session *)
   309 
   310 fun isatool_document doc_format doc_prefix =
   311   let
   312     val cmd = "$ISATOOL document -c -o '" ^ doc_format ^ "' '" ^ File.sysify_path doc_prefix ^ "'";
   313   in
   314     writeln cmd;
   315     if system cmd <> 0 orelse not (File.exists (Path.ext doc_format doc_prefix)) then
   316       error "Failed to build document"
   317     else ()
   318   end;
   319 
   320 fun write_tex src name path = Buffer.write (Path.append path (tex_path name)) src;
   321 
   322 fun write_texes src name (path, None) = write_tex src name path
   323   | write_texes src name (path, Some path') = (write_tex src name path; write_tex src name path');
   324 
   325 
   326 fun finish () = with_session ()
   327     (fn {name, html_prefix, doc_format, doc_prefixes, path, ...} =>
   328   let
   329     val {theories, tex_index, html_index, graph} = ! browser_info;
   330     val parent_html_prefix = Path.append html_prefix Path.parent;
   331 
   332     fun finish_node (a, {tex_source, html_source = _, html}) =
   333      (doc_prefixes |> apsome (write_texes tex_source a);
   334       Buffer.write (Path.append html_prefix (html_path a)) (Buffer.add HTML.end_theory html));
   335   in
   336     seq finish_node (Symtab.dest theories);
   337     Buffer.write (Path.append html_prefix pre_index_path) html_index;
   338     doc_prefixes |> apsome (write_texes tex_index doc_indexN);
   339     doc_prefixes |> apsome (isatool_document doc_format o #1);
   340     write_graph graph (Path.append html_prefix (graph_path "session"));
   341     create_index html_prefix;
   342     if length path > 1 then update_index parent_html_prefix name else ();
   343     browser_info := empty_browser_info;
   344     session_info := None
   345   end);
   346 
   347 
   348 (* theory elements *)
   349 
   350 fun init_theory name = with_session () (fn _ => init_theory_info name empty_theory_info);
   351 
   352 fun verbatim_source name mk_text =
   353   with_session () (fn _ => add_html_source name (HTML.verbatim_source (mk_text ())));
   354 
   355 fun old_symbol_source name mk_text =
   356   with_session () (fn _ => add_tex_source name (Latex.old_symbol_source name (mk_text ())));
   357 
   358 fun theory_output name s =
   359   with_session () (fn _ => add_tex_source name (Latex.isabelle_file s));
   360 
   361 
   362 fun parent_link remote_path curr_session name =
   363   let val {name = _, session, is_local} = get_info (ThyInfo.theory name)
   364   in (if null session then None else
   365      Some (if is_some remote_path andalso not is_local then
   366        Url.append (the remote_path) (Url.file
   367          (Path.append (Path.make session) (html_path name)))
   368      else Url.file (Path.append (mk_rel_path curr_session session)
   369        (html_path name))), name)
   370   end;
   371 
   372 fun begin_theory name raw_parents orig_files thy =
   373     with_session thy (fn {name = sess_name, session, path, html_prefix, remote_path, ...} =>
   374   let
   375     val parents = map (parent_link remote_path path) raw_parents;
   376     val ml_path = ThyLoad.ml_path name;
   377     val files = map (apsnd Some) orig_files @
   378       (if is_some (ThyLoad.check_file ml_path) then [(ml_path, None)] else []);
   379 
   380     fun prep_file (raw_path, loadit) =
   381       (case ThyLoad.check_file raw_path of
   382         Some (path, _) =>
   383           let
   384             val base = Path.base path;
   385             val base_html = html_ext base;
   386           in
   387             File.write (Path.append html_prefix base_html)
   388               (HTML.ml_file (Url.file base) (File.read path));
   389             (Some (Url.file base_html), Url.file raw_path, loadit)
   390           end
   391       | None => (warning ("Browser info: expected to find ML file" ^ quote (Path.pack raw_path));
   392           (None, Url.file raw_path, loadit)));
   393 
   394     val files_html = map prep_file files;
   395 
   396     fun prep_html_source (tex_source, html_source, html) =
   397       let
   398         val txt = HTML.begin_theory (Url.file index_path, session)
   399           name parents files_html (Buffer.content html_source)
   400       in (tex_source, Buffer.empty, Buffer.add txt html) end;
   401 
   402     val entry =
   403      {name = name, ID = ID_of path name, dir = sess_name, unfold = true,
   404       path = Path.pack (html_path name),
   405       parents = map (fn s => ID_of (#session (get_info (ThyInfo.theory s))) s) raw_parents};
   406 
   407   in
   408     change_theory_info name prep_html_source;
   409     add_graph_entry entry;
   410     add_html_index (HTML.theory_entry (Url.file (html_path name), name));
   411     add_tex_index (Latex.theory_entry name);
   412     BrowserInfoData.put {name = sess_name, session = path, is_local = is_some remote_path} thy
   413   end);
   414 
   415 
   416 fun result k a thm = with_session () (fn _ => with_context add_html (HTML.result k a thm));
   417 fun results k a thms = with_session () (fn _ => with_context add_html (HTML.results k a thms));
   418 fun theorem a thm = with_session () (fn _ => with_context add_html (HTML.theorem a thm));
   419 fun theorems a thms = with_session () (fn _ => with_context add_html (HTML.theorems a thms));
   420 fun chapter s = with_session () (fn _ => with_context add_html (HTML.chapter s));
   421 fun section s = with_session () (fn _ => with_context add_html (HTML.section s));
   422 fun subsection s = with_session () (fn _ => with_context add_html (HTML.subsection s));
   423 fun subsubsection s = with_session () (fn _ => with_context add_html (HTML.subsubsection s));
   424 
   425 
   426 
   427 (** theory setup **)
   428 
   429 val setup = [BrowserInfoData.init];
   430 
   431 
   432 end;
   433 
   434 
   435 structure BasicPresent: BASIC_PRESENT = Present;
   436 open BasicPresent;