author | wenzelm |
Wed, 12 Nov 1997 16:22:59 +0100 | |
changeset 4215 | 7f7519759b8c |
parent 3976 | 1030dd79720b |
child 4567 | b0b963a01a0c |
permissions | -rw-r--r-- |
3603
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
1 |
(* Title: Pure/Thy/thy_browser_info.ML |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
2 |
ID: $Id$ |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
3 |
Author: Stefan Berghofer and Carsten Clasohm |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
4 |
Copyright 1994, 1997 TU Muenchen |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
5 |
|
3870 | 6 |
The first design of the text-based html browser is due to Mateja Jamnik. |
7 |
||
3603
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
8 |
Functions for generating theory browsing information |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
9 |
(i.e. *.html and *.graph - files). |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
10 |
*) |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
11 |
|
4215
7f7519759b8c
moved old file stuff from library.ML to Thy/browser_info.ML;
wenzelm
parents:
3976
diff
changeset
|
12 |
|
7f7519759b8c
moved old file stuff from library.ML to Thy/browser_info.ML;
wenzelm
parents:
3976
diff
changeset
|
13 |
(** filenames and paths **) (* FIXME FIXME FIXME eliminate!!! *) |
7f7519759b8c
moved old file stuff from library.ML to Thy/browser_info.ML;
wenzelm
parents:
3976
diff
changeset
|
14 |
|
7f7519759b8c
moved old file stuff from library.ML to Thy/browser_info.ML;
wenzelm
parents:
3976
diff
changeset
|
15 |
(*BAD_space_explode "." "h.e..l.lo"; gives ["h", "e", "l", "lo"]*) |
7f7519759b8c
moved old file stuff from library.ML to Thy/browser_info.ML;
wenzelm
parents:
3976
diff
changeset
|
16 |
fun BAD_space_explode sep s = |
7f7519759b8c
moved old file stuff from library.ML to Thy/browser_info.ML;
wenzelm
parents:
3976
diff
changeset
|
17 |
let fun divide [] "" = [] |
7f7519759b8c
moved old file stuff from library.ML to Thy/browser_info.ML;
wenzelm
parents:
3976
diff
changeset
|
18 |
| divide [] part = [part] |
7f7519759b8c
moved old file stuff from library.ML to Thy/browser_info.ML;
wenzelm
parents:
3976
diff
changeset
|
19 |
| divide (c::s) part = |
7f7519759b8c
moved old file stuff from library.ML to Thy/browser_info.ML;
wenzelm
parents:
3976
diff
changeset
|
20 |
if c = sep then |
7f7519759b8c
moved old file stuff from library.ML to Thy/browser_info.ML;
wenzelm
parents:
3976
diff
changeset
|
21 |
(if part = "" then divide s "" else part :: divide s "") |
7f7519759b8c
moved old file stuff from library.ML to Thy/browser_info.ML;
wenzelm
parents:
3976
diff
changeset
|
22 |
else divide s (part ^ c) |
7f7519759b8c
moved old file stuff from library.ML to Thy/browser_info.ML;
wenzelm
parents:
3976
diff
changeset
|
23 |
in divide (explode s) "" end; |
7f7519759b8c
moved old file stuff from library.ML to Thy/browser_info.ML;
wenzelm
parents:
3976
diff
changeset
|
24 |
|
7f7519759b8c
moved old file stuff from library.ML to Thy/browser_info.ML;
wenzelm
parents:
3976
diff
changeset
|
25 |
(*Convert UNIX filename of the form "path/file" to "path/" and "file"; |
7f7519759b8c
moved old file stuff from library.ML to Thy/browser_info.ML;
wenzelm
parents:
3976
diff
changeset
|
26 |
if filename contains no slash, then it returns "" and "file"*) |
7f7519759b8c
moved old file stuff from library.ML to Thy/browser_info.ML;
wenzelm
parents:
3976
diff
changeset
|
27 |
val split_filename = |
7f7519759b8c
moved old file stuff from library.ML to Thy/browser_info.ML;
wenzelm
parents:
3976
diff
changeset
|
28 |
(pairself implode) o take_suffix (not_equal "/") o explode; |
7f7519759b8c
moved old file stuff from library.ML to Thy/browser_info.ML;
wenzelm
parents:
3976
diff
changeset
|
29 |
|
7f7519759b8c
moved old file stuff from library.ML to Thy/browser_info.ML;
wenzelm
parents:
3976
diff
changeset
|
30 |
val base_name = #2 o split_filename; |
7f7519759b8c
moved old file stuff from library.ML to Thy/browser_info.ML;
wenzelm
parents:
3976
diff
changeset
|
31 |
|
7f7519759b8c
moved old file stuff from library.ML to Thy/browser_info.ML;
wenzelm
parents:
3976
diff
changeset
|
32 |
(*Merge splitted filename (path and file); |
7f7519759b8c
moved old file stuff from library.ML to Thy/browser_info.ML;
wenzelm
parents:
3976
diff
changeset
|
33 |
if path does not end with one a slash is appended*) |
7f7519759b8c
moved old file stuff from library.ML to Thy/browser_info.ML;
wenzelm
parents:
3976
diff
changeset
|
34 |
fun tack_on "" name = name |
7f7519759b8c
moved old file stuff from library.ML to Thy/browser_info.ML;
wenzelm
parents:
3976
diff
changeset
|
35 |
| tack_on path name = |
7f7519759b8c
moved old file stuff from library.ML to Thy/browser_info.ML;
wenzelm
parents:
3976
diff
changeset
|
36 |
if last_elem (explode path) = "/" then path ^ name |
7f7519759b8c
moved old file stuff from library.ML to Thy/browser_info.ML;
wenzelm
parents:
3976
diff
changeset
|
37 |
else path ^ "/" ^ name; |
7f7519759b8c
moved old file stuff from library.ML to Thy/browser_info.ML;
wenzelm
parents:
3976
diff
changeset
|
38 |
|
7f7519759b8c
moved old file stuff from library.ML to Thy/browser_info.ML;
wenzelm
parents:
3976
diff
changeset
|
39 |
(*Remove the extension of a filename, i.e. the part after the last '.'*) |
7f7519759b8c
moved old file stuff from library.ML to Thy/browser_info.ML;
wenzelm
parents:
3976
diff
changeset
|
40 |
val remove_ext = implode o #1 o take_suffix (not_equal ".") o explode; |
7f7519759b8c
moved old file stuff from library.ML to Thy/browser_info.ML;
wenzelm
parents:
3976
diff
changeset
|
41 |
|
7f7519759b8c
moved old file stuff from library.ML to Thy/browser_info.ML;
wenzelm
parents:
3976
diff
changeset
|
42 |
(*Make relative path to reach an absolute location from a different one*) |
7f7519759b8c
moved old file stuff from library.ML to Thy/browser_info.ML;
wenzelm
parents:
3976
diff
changeset
|
43 |
fun relative_path cur_path dest_path = |
7f7519759b8c
moved old file stuff from library.ML to Thy/browser_info.ML;
wenzelm
parents:
3976
diff
changeset
|
44 |
let (*Remove common beginning of both paths and make relative path*) |
7f7519759b8c
moved old file stuff from library.ML to Thy/browser_info.ML;
wenzelm
parents:
3976
diff
changeset
|
45 |
fun mk_relative [] [] = [] |
7f7519759b8c
moved old file stuff from library.ML to Thy/browser_info.ML;
wenzelm
parents:
3976
diff
changeset
|
46 |
| mk_relative [] ds = ds |
7f7519759b8c
moved old file stuff from library.ML to Thy/browser_info.ML;
wenzelm
parents:
3976
diff
changeset
|
47 |
| mk_relative cs [] = map (fn _ => "..") cs |
7f7519759b8c
moved old file stuff from library.ML to Thy/browser_info.ML;
wenzelm
parents:
3976
diff
changeset
|
48 |
| mk_relative (c::cs) (d::ds) = |
7f7519759b8c
moved old file stuff from library.ML to Thy/browser_info.ML;
wenzelm
parents:
3976
diff
changeset
|
49 |
if c = d then mk_relative cs ds |
7f7519759b8c
moved old file stuff from library.ML to Thy/browser_info.ML;
wenzelm
parents:
3976
diff
changeset
|
50 |
else ".." :: map (fn _ => "..") cs @ (d::ds); |
7f7519759b8c
moved old file stuff from library.ML to Thy/browser_info.ML;
wenzelm
parents:
3976
diff
changeset
|
51 |
in if cur_path = "" orelse hd (explode cur_path) <> "/" orelse |
7f7519759b8c
moved old file stuff from library.ML to Thy/browser_info.ML;
wenzelm
parents:
3976
diff
changeset
|
52 |
dest_path = "" orelse hd (explode dest_path) <> "/" then |
7f7519759b8c
moved old file stuff from library.ML to Thy/browser_info.ML;
wenzelm
parents:
3976
diff
changeset
|
53 |
error "Relative or empty path passed to relative_path" |
7f7519759b8c
moved old file stuff from library.ML to Thy/browser_info.ML;
wenzelm
parents:
3976
diff
changeset
|
54 |
else (); |
7f7519759b8c
moved old file stuff from library.ML to Thy/browser_info.ML;
wenzelm
parents:
3976
diff
changeset
|
55 |
space_implode "/" (mk_relative (BAD_space_explode "/" cur_path) |
7f7519759b8c
moved old file stuff from library.ML to Thy/browser_info.ML;
wenzelm
parents:
3976
diff
changeset
|
56 |
(BAD_space_explode "/" dest_path)) |
7f7519759b8c
moved old file stuff from library.ML to Thy/browser_info.ML;
wenzelm
parents:
3976
diff
changeset
|
57 |
end; |
7f7519759b8c
moved old file stuff from library.ML to Thy/browser_info.ML;
wenzelm
parents:
3976
diff
changeset
|
58 |
|
7f7519759b8c
moved old file stuff from library.ML to Thy/browser_info.ML;
wenzelm
parents:
3976
diff
changeset
|
59 |
(*Determine if absolute path1 is a subdirectory of absolute path2*) |
7f7519759b8c
moved old file stuff from library.ML to Thy/browser_info.ML;
wenzelm
parents:
3976
diff
changeset
|
60 |
fun subdir_of (path1, path2) = |
7f7519759b8c
moved old file stuff from library.ML to Thy/browser_info.ML;
wenzelm
parents:
3976
diff
changeset
|
61 |
if hd (explode path1) <> "/" orelse hd (explode path2) <> "/" then |
7f7519759b8c
moved old file stuff from library.ML to Thy/browser_info.ML;
wenzelm
parents:
3976
diff
changeset
|
62 |
error "Relative or empty path passed to subdir_of" |
7f7519759b8c
moved old file stuff from library.ML to Thy/browser_info.ML;
wenzelm
parents:
3976
diff
changeset
|
63 |
else (BAD_space_explode "/" path2) prefix (BAD_space_explode "/" path1); |
7f7519759b8c
moved old file stuff from library.ML to Thy/browser_info.ML;
wenzelm
parents:
3976
diff
changeset
|
64 |
|
7f7519759b8c
moved old file stuff from library.ML to Thy/browser_info.ML;
wenzelm
parents:
3976
diff
changeset
|
65 |
fun absolute_path cwd file = |
7f7519759b8c
moved old file stuff from library.ML to Thy/browser_info.ML;
wenzelm
parents:
3976
diff
changeset
|
66 |
let fun rm_points [] result = rev result |
7f7519759b8c
moved old file stuff from library.ML to Thy/browser_info.ML;
wenzelm
parents:
3976
diff
changeset
|
67 |
| rm_points (".."::ds) result = rm_points ds (tl result) |
7f7519759b8c
moved old file stuff from library.ML to Thy/browser_info.ML;
wenzelm
parents:
3976
diff
changeset
|
68 |
| rm_points ("."::ds) result = rm_points ds result |
7f7519759b8c
moved old file stuff from library.ML to Thy/browser_info.ML;
wenzelm
parents:
3976
diff
changeset
|
69 |
| rm_points (d::ds) result = rm_points ds (d::result); |
7f7519759b8c
moved old file stuff from library.ML to Thy/browser_info.ML;
wenzelm
parents:
3976
diff
changeset
|
70 |
in if file = "" then "" |
7f7519759b8c
moved old file stuff from library.ML to Thy/browser_info.ML;
wenzelm
parents:
3976
diff
changeset
|
71 |
else if hd (explode file) = "/" then file |
7f7519759b8c
moved old file stuff from library.ML to Thy/browser_info.ML;
wenzelm
parents:
3976
diff
changeset
|
72 |
else "/" ^ space_implode "/" |
7f7519759b8c
moved old file stuff from library.ML to Thy/browser_info.ML;
wenzelm
parents:
3976
diff
changeset
|
73 |
(rm_points (BAD_space_explode "/" (tack_on cwd file)) []) |
7f7519759b8c
moved old file stuff from library.ML to Thy/browser_info.ML;
wenzelm
parents:
3976
diff
changeset
|
74 |
end; |
7f7519759b8c
moved old file stuff from library.ML to Thy/browser_info.ML;
wenzelm
parents:
3976
diff
changeset
|
75 |
|
7f7519759b8c
moved old file stuff from library.ML to Thy/browser_info.ML;
wenzelm
parents:
3976
diff
changeset
|
76 |
|
7f7519759b8c
moved old file stuff from library.ML to Thy/browser_info.ML;
wenzelm
parents:
3976
diff
changeset
|
77 |
|
3603
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
78 |
signature BROWSER_INFO = |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
79 |
sig |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
80 |
val output_dir : string ref |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
81 |
val home_path : string ref |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
82 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
83 |
val make_graph : bool ref |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
84 |
val init_graph : string -> unit |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
85 |
val mk_graph : string -> string -> unit |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
86 |
val cur_thyname : string ref |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
87 |
val make_html : bool ref |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
88 |
val mk_html : string -> string -> string list -> unit |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
89 |
val thyfile2html : string -> string -> unit |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
90 |
val init_html : unit -> unit |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
91 |
val finish_html : unit -> unit |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
92 |
val section : string -> unit |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
93 |
val thm_to_html : thm -> string -> unit |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
94 |
val close_html : unit -> unit |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
95 |
end; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
96 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
97 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
98 |
structure BrowserInfo : BROWSER_INFO = |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
99 |
struct |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
100 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
101 |
open ThyInfo; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
102 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
103 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
104 |
(*directory where to put html and graph files*) |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
105 |
val output_dir = ref ""; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
106 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
107 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
108 |
(*path of user home directory*) |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
109 |
val home_path = ref ""; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
110 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
111 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
112 |
(*normalize a path |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
113 |
FIXME: move to library?*) |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
114 |
fun normalize_path p = |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
115 |
let val curr_dir = pwd (); |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
116 |
val _ = cd p; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
117 |
val norm_path = pwd (); |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
118 |
val _ = cd curr_dir |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
119 |
in norm_path end; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
120 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
121 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
122 |
(*create directory |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
123 |
FIXME: move to library?*) |
3628 | 124 |
fun mkdir path = (execute ("mkdir -p " ^ path); ()); |
3603
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
125 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
126 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
127 |
(*Path of Isabelle's main (source) directory |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
128 |
FIXME: this value should be provided by isatool!*) |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
129 |
val base_path = ref ( |
3834 | 130 |
"/" ^ space_implode "/" (rev (tl (tl (rev (BAD_space_explode "/" (OS.FileSys.getDir ()))))))); |
3603
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
131 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
132 |
|
3628 | 133 |
|
3603
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
134 |
(******************** HTML generation functions *************************) |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
135 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
136 |
(*Set location of graphics for HTML files*) |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
137 |
fun gif_path () = tack_on (normalize_path (!output_dir)) "gif"; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
138 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
139 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
140 |
(*Name of theory currently being read*) |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
141 |
val cur_thyname = ref ""; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
142 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
143 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
144 |
(*Name of current logic*) |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
145 |
val package = ref ""; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
146 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
147 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
148 |
(* Return path of directory where to store html / graph data |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
149 |
corresponding to theory with given path *) |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
150 |
local |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
151 |
fun make_path q p = |
3748
e5d2399a154f
Changed html data directory and names of graph files.
berghofe
parents:
3639
diff
changeset
|
152 |
let val outp_dir = normalize_path (!output_dir); |
e5d2399a154f
Changed html data directory and names of graph files.
berghofe
parents:
3639
diff
changeset
|
153 |
val base = if q = "" then outp_dir else tack_on outp_dir q; |
4215
7f7519759b8c
moved old file stuff from library.ML to Thy/browser_info.ML;
wenzelm
parents:
3976
diff
changeset
|
154 |
val rpath = if subdir_of (p, !base_path) then relative_path (!base_path) p |
3603
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
155 |
else relative_path (normalize_path (!home_path)) p; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
156 |
in tack_on base rpath end |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
157 |
in |
3748
e5d2399a154f
Changed html data directory and names of graph files.
berghofe
parents:
3639
diff
changeset
|
158 |
val html_path = make_path ""; |
3639 | 159 |
val graph_path = make_path "graph/data" |
3603
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
160 |
end; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
161 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
162 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
163 |
(*Location of theory-list.txt and index.html (set by init_html)*) |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
164 |
val index_path = ref ""; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
165 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
166 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
167 |
(*Original path of ROOT.ML*) |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
168 |
val original_path = ref ""; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
169 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
170 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
171 |
(*Location of Pure_sub.html and CPure_sub.html*) |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
172 |
val pure_subchart = ref (None : string option); |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
173 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
174 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
175 |
(*Controls whether HTML files should be generated*) |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
176 |
val make_html = ref false; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
177 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
178 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
179 |
(*HTML file of theory currently being read |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
180 |
(Initialized by thyfile2html; used by use_thy and store_thm)*) |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
181 |
val cur_htmlfile = ref None : TextIO.outstream option ref; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
182 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
183 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
184 |
(*Boolean variable which indicates if the title "Theorems proved in foo.ML" |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
185 |
has already been inserted into the current HTML file*) |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
186 |
val cur_has_title = ref false; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
187 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
188 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
189 |
(*Make head of HTML dependency charts |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
190 |
Parameters are: |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
191 |
file: HTML file |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
192 |
tname: theory name |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
193 |
suffix: suffix of complementary chart |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
194 |
(sup if this head is for a sub-chart, sub if it is for a sup-chart; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
195 |
empty for Pure and CPure sub-charts) |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
196 |
gif_path: relative path to directory containing GIFs |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
197 |
index_path: relative path to directory containing main theory chart |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
198 |
*) |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
199 |
fun mk_charthead file tname title repeats gif_path index_path package = |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
200 |
TextIO.output (file, |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
201 |
"<HTML><HEAD><TITLE>" ^ title ^ " of " ^ tname ^ |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
202 |
"</TITLE></HEAD>\n<H2>" ^ title ^ " of theory " ^ tname ^ |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
203 |
"</H2>\nThe name of every theory is linked to its theory file<BR>\n" ^ |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
204 |
"<IMG SRC = \"" ^ tack_on gif_path "red_arrow.gif\ |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
205 |
\\" ALT = \\/></A> stands for subtheories (child theories)<BR>\n\ |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
206 |
\<IMG SRC = \"" ^ tack_on gif_path "blue_arrow.gif\ |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
207 |
\\" ALT = /\\></A> stands for supertheories (parent theories)\n" ^ |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
208 |
(if not repeats then "" else |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
209 |
"<BR><TT>...</TT> stands for repeated subtrees") ^ |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
210 |
"<P>\n<A HREF = \"" ^ tack_on index_path "index.html\ |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
211 |
\\">Back</A> to the index of " ^ package ^ "\n<HR>\n<PRE>"); |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
212 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
213 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
214 |
(*Convert special HTML characters ('&', '>', and '<')*) |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
215 |
fun escape [] = [] |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
216 |
| escape ("<"::s) = "<" :: escape s |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
217 |
| escape (">"::s) = ">" :: escape s |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
218 |
| escape ("&"::s) = "&" :: escape s |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
219 |
| escape (c::s) = c :: escape s; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
220 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
221 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
222 |
(*Convert .thy file to HTML and make chart of its super-theories*) |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
223 |
fun thyfile2html tname thy_path = if not (!make_html) then () else |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
224 |
let |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
225 |
(* path of directory, where corresponding HTML file is stored *) |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
226 |
val tpath = html_path thy_path; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
227 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
228 |
(* gif directory *) |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
229 |
val rel_gif_path = relative_path tpath (gif_path ()); |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
230 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
231 |
val rel_index_path = relative_path tpath (!index_path); |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
232 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
233 |
(*Make list of all theories and all theories that own a .thy file*) |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
234 |
fun list_theories [] theories thy_files = (theories, thy_files) |
3976 | 235 |
| list_theories ((tname, {thy_time, ...}: thy_info) :: ts) |
3603
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
236 |
theories thy_files = |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
237 |
list_theories ts (tname :: theories) |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
238 |
(if is_some thy_time andalso the thy_time <> "" then |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
239 |
tname :: thy_files |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
240 |
else thy_files); |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
241 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
242 |
val (theories, thy_files) = |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
243 |
list_theories (Symtab.dest (!loaded_thys)) [] []; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
244 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
245 |
(*convert ML file to html *) |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
246 |
fun ml2html name abs_path = |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
247 |
let val is = TextIO.openIn (tack_on abs_path (name ^ ".ML")); |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
248 |
val inp = implode (escape (explode (TextIO.inputAll is))); |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
249 |
val _ = TextIO.closeIn is; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
250 |
val os = TextIO.openOut (tack_on (html_path abs_path) (name ^ "_ML.html")); |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
251 |
val _ = TextIO.output (os, |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
252 |
"<HTML><HEAD><TITLE>" ^ name ^ ".ML</TITLE></HEAD>\n\n<BODY>\n" ^ |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
253 |
"<H2>" ^ name ^ ".ML</H2>\n<A HREF = \"" ^ |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
254 |
name ^ ".html\">Back</A> to theory " ^ name ^ |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
255 |
"\n<HR>\n\n<PRE>\n" ^ inp ^ "</PRE><HR></BODY></HTML>"); |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
256 |
val _ = TextIO.closeOut os; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
257 |
in () end; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
258 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
259 |
(*Do the conversion*) |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
260 |
fun gettext thy_file = |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
261 |
let |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
262 |
(*Convert special HTML characters ('&', '>', and '<')*) |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
263 |
val file = |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
264 |
let val is = TextIO.openIn thy_file; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
265 |
val inp = TextIO.inputAll is; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
266 |
in (TextIO.closeIn is; escape (explode inp)) end; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
267 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
268 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
269 |
(*Isolate first (possibly nested) comment; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
270 |
skip all leading whitespaces*) |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
271 |
val (comment, file') = |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
272 |
let fun first_comment ("*" :: ")" :: cs) co 1 = (co ^ "*)", cs) |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
273 |
| first_comment ("*" :: ")" :: cs) co d = |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
274 |
first_comment cs (co ^ "*)") (d-1) |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
275 |
| first_comment ("(" :: "*" :: cs) co d = |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
276 |
first_comment cs (co ^ "(*") (d+1) |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
277 |
| first_comment (" " :: cs) "" 0 = first_comment cs "" 0 |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
278 |
| first_comment ("\n" :: cs) "" 0 = first_comment cs "" 0 |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
279 |
| first_comment ("\t" :: cs) "" 0 = first_comment cs "" 0 |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
280 |
| first_comment cs "" 0 = ("", cs) |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
281 |
| first_comment (c :: cs) co d = |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
282 |
first_comment cs (co ^ implode [c]) d |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
283 |
| first_comment [] co _ = |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
284 |
error ("Unexpected end of file " ^ tname ^ ".thy."); |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
285 |
in first_comment file "" 0 end; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
286 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
287 |
(*Process line defining theory's ancestors; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
288 |
convert valid theory names to links to their HTML file*) |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
289 |
val (ancestors, body) = |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
290 |
let |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
291 |
fun make_links l result = |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
292 |
let val (pre, letter) = take_prefix (not o is_letter) l; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
293 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
294 |
val (id, rest) = |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
295 |
take_prefix (is_quasi_letter orf is_digit) letter; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
296 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
297 |
val id = implode id; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
298 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
299 |
(*Make a HTML link out of a theory name*) |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
300 |
fun make_link t = |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
301 |
let val path = html_path (path_of t); |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
302 |
in "<A HREF = \"" ^ |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
303 |
tack_on (relative_path tpath path) t ^ |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
304 |
".html\">" ^ t ^ "</A>" end; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
305 |
in if not (id mem theories) then (result, implode l) |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
306 |
else if id mem thy_files then |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
307 |
make_links rest (result ^ implode pre ^ make_link id) |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
308 |
else make_links rest (result ^ implode pre ^ id) |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
309 |
end; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
310 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
311 |
val (pre, rest) = take_prefix (fn c => c <> "=") file'; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
312 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
313 |
val (ancestors, body) = |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
314 |
if null rest then |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
315 |
error ("Missing \"=\" in file " ^ tname ^ ".thy.\n\ |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
316 |
\(Make sure that the last line ends with a linebreak.)") |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
317 |
else |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
318 |
make_links rest ""; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
319 |
in (implode pre ^ ancestors, body) end; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
320 |
in "<HTML><HEAD><TITLE>" ^ tname ^ ".thy</TITLE></HEAD>\n\n<BODY>\n" ^ |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
321 |
"<H2>" ^ tname ^ ".thy</H2>\n<A HREF = \"" ^ |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
322 |
tack_on rel_index_path "index.html\ |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
323 |
\\">Back</A> to the index of " ^ (!package) ^ |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
324 |
"\n<HR>\n\n<PRE>\n" ^ comment ^ ancestors ^ body ^ |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
325 |
"</PRE>\n" |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
326 |
end; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
327 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
328 |
(** Make chart of super-theories **) |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
329 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
330 |
val _ = mkdir tpath; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
331 |
val sup_out = TextIO.openOut (tack_on tpath (tname ^ "_sup.html")); |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
332 |
val sub_out = TextIO.openOut (tack_on tpath (tname ^ "_sub.html")); |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
333 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
334 |
(*Theories that already have been listed in this chart*) |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
335 |
val listed = ref []; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
336 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
337 |
val wanted_theories = |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
338 |
filter (fn s => s mem thy_files orelse s = "Pure" orelse s = "CPure") |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
339 |
theories; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
340 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
341 |
(*Make tree of theory dependencies*) |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
342 |
fun list_ancestors tname level continued = |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
343 |
let |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
344 |
fun mk_entry [] = () |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
345 |
| mk_entry (t::ts) = |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
346 |
let |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
347 |
val is_pure = t = "Pure" orelse t = "CPure"; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
348 |
val path = if is_pure then (the (!pure_subchart)) |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
349 |
else html_path (path_of t); |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
350 |
val rel_path = relative_path tpath path; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
351 |
val repeated = t mem (!listed) andalso |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
352 |
not (null (parents_of_name t)); |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
353 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
354 |
fun mk_offset [] cur = |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
355 |
if level < cur then error "Error in mk_offset" |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
356 |
else implode (replicate (level - cur) " ") |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
357 |
| mk_offset (l::ls) cur = |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
358 |
implode (replicate (l - cur) " ") ^ "| " ^ |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
359 |
mk_offset ls (l+1); |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
360 |
in TextIO.output (sup_out, |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
361 |
" " ^ mk_offset continued 0 ^ |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
362 |
"\\__" ^ (if is_pure then t else |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
363 |
"<A HREF=\"" ^ tack_on rel_path t ^ |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
364 |
".html\">" ^ t ^ "</A>") ^ |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
365 |
(if repeated then "..." else " ") ^ |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
366 |
"<A HREF = \"" ^ tack_on rel_path t ^ |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
367 |
"_sub.html\"><IMG ALIGN=BOTTOM BORDER=0 SRC = \"" ^ |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
368 |
tack_on rel_gif_path "red_arrow.gif\" ALT = \\/></A>" ^ |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
369 |
(if is_pure then "" |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
370 |
else "<A HREF = \"" ^ tack_on rel_path t ^ |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
371 |
"_sup.html\"><IMG ALIGN=BOTTOM BORDER=0 SRC = \"" ^ |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
372 |
tack_on rel_gif_path "blue_arrow.gif\ |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
373 |
\\" ALT = /\\></A>") ^ |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
374 |
"\n"); |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
375 |
if repeated then () |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
376 |
else (listed := t :: (!listed); |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
377 |
list_ancestors t (level+1) (if null ts then continued |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
378 |
else continued @ [level]); |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
379 |
mk_entry ts) |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
380 |
end; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
381 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
382 |
val relatives = |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
383 |
filter (fn s => s mem wanted_theories) (parents_of_name tname); |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
384 |
in mk_entry relatives end; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
385 |
in if is_some (!cur_htmlfile) then |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
386 |
(TextIO.closeOut (the (!cur_htmlfile)); |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
387 |
warning "Last theory's HTML file has not been closed.") |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
388 |
else (); |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
389 |
cur_htmlfile := Some (TextIO.openOut (tack_on tpath (tname ^ ".html"))); |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
390 |
cur_has_title := false; |
4215
7f7519759b8c
moved old file stuff from library.ML to Thy/browser_info.ML;
wenzelm
parents:
3976
diff
changeset
|
391 |
if File.exists (tack_on thy_path (tname ^ ".ML")) |
3603
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
392 |
then ml2html tname thy_path else (); |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
393 |
TextIO.output (the (!cur_htmlfile), gettext (tack_on thy_path tname ^ ".thy")); |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
394 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
395 |
mk_charthead sup_out tname "Ancestors" true rel_gif_path rel_index_path |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
396 |
(!package); |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
397 |
TextIO.output(sup_out, |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
398 |
"<A HREF=\"" ^ tname ^ ".html\">" ^ tname ^ "</A> \ |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
399 |
\<A HREF = \"" ^ tname ^ |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
400 |
"_sub.html\"><IMG ALIGN=BOTTOM BORDER=0 SRC = \"" ^ |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
401 |
tack_on rel_gif_path "red_arrow.gif\" ALT = \\/></A>\n"); |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
402 |
list_ancestors tname 0 []; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
403 |
TextIO.output (sup_out, "</PRE><HR></BODY></HTML>"); |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
404 |
TextIO.closeOut sup_out; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
405 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
406 |
mk_charthead sub_out tname "Children" false rel_gif_path rel_index_path |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
407 |
(!package); |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
408 |
TextIO.output(sub_out, |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
409 |
"<A HREF=\"" ^ tname ^ ".html\">" ^ tname ^ "</A> \ |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
410 |
\<A HREF = \"" ^ tname ^ "_sup.html\"><IMG SRC = \"" ^ |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
411 |
tack_on rel_gif_path "blue_arrow.gif\" BORDER=0 ALT = \\/></A>\n"); |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
412 |
TextIO.closeOut sub_out |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
413 |
end; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
414 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
415 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
416 |
(*Makes HTML title for list of theorems; as this list may be empty and we |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
417 |
don't want a title in that case, mk_theorems_title is only invoked when |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
418 |
something is added to the list*) |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
419 |
fun mk_theorems_title out = |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
420 |
if not (!cur_has_title) then |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
421 |
(cur_has_title := true; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
422 |
TextIO.output (out, "<HR><H2>Theorems proved in <A HREF = \"" ^ |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
423 |
(!cur_thyname) ^ "_ML.html\">" ^ (!cur_thyname) ^ |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
424 |
".ML</A>:</H2>\n")) |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
425 |
else (); |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
426 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
427 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
428 |
exception MK_HTML; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
429 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
430 |
(*Add theory to file listing all loaded theories (for index.html) |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
431 |
and to the sub-charts of its parents*) |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
432 |
fun mk_html tname abs_path old_parents = if not (!make_html) then () else |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
433 |
( let val new_parents = parents_of_name tname \\ old_parents; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
434 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
435 |
fun robust_seq (proc: 'a -> unit) : 'a list -> unit = |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
436 |
let fun seqf [] = () |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
437 |
| seqf (x :: xs) = (proc x handle _ => (); seqf xs) |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
438 |
in seqf end; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
439 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
440 |
(*Add child to parents' sub-theory charts*) |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
441 |
fun add_to_parents t = |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
442 |
let val path = if t = "Pure" orelse t = "CPure" then |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
443 |
(the (!pure_subchart)) |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
444 |
else html_path (path_of t); |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
445 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
446 |
val rel_gif_path = relative_path path (gif_path ()); |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
447 |
val rel_path = relative_path path (html_path abs_path); |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
448 |
val tpath = tack_on rel_path tname; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
449 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
450 |
val fname = tack_on path (t ^ "_sub.html"); |
4215
7f7519759b8c
moved old file stuff from library.ML to Thy/browser_info.ML;
wenzelm
parents:
3976
diff
changeset
|
451 |
val out = if File.exists fname then |
3603
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
452 |
TextIO.openAppend fname handle e => |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
453 |
(warning ("Unable to write to file " ^ |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
454 |
fname); raise e) |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
455 |
else raise MK_HTML; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
456 |
in TextIO.output (out, |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
457 |
" |\n \\__<A HREF=\"" ^ |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
458 |
tack_on rel_path tname ^ ".html\">" ^ tname ^ |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
459 |
"</A> <A HREF = \"" ^ tpath ^ "_sub.html\">\ |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
460 |
\<IMG ALIGN=BOTTOM BORDER=0 SRC = \"" ^ |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
461 |
tack_on rel_gif_path "red_arrow.gif\" ALT = \\/></A>\ |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
462 |
\<A HREF = \"" ^ tpath ^ "_sup.html\">\ |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
463 |
\<IMG ALIGN=BOTTOM BORDER=0 SRC = \"" ^ |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
464 |
tack_on rel_gif_path "blue_arrow.gif\" ALT = /\\></A>\n"); |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
465 |
TextIO.closeOut out |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
466 |
end; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
467 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
468 |
val theory_list = |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
469 |
TextIO.openAppend (tack_on (!index_path) "theory_list.txt") |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
470 |
handle _ => (make_html := false; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
471 |
warning ("Cannot write to " ^ |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
472 |
(!index_path) ^ " while making HTML files.\n\ |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
473 |
\HTML generation has been switched off.\n\ |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
474 |
\Call init_html() from within a \ |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
475 |
\writeable directory to reactivate it."); |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
476 |
raise MK_HTML) |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
477 |
in TextIO.output (theory_list, tname ^ " " ^ abs_path ^ "\n"); |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
478 |
TextIO.closeOut theory_list; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
479 |
robust_seq add_to_parents new_parents |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
480 |
end |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
481 |
) handle MK_HTML => (); |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
482 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
483 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
484 |
(*** Misc HTML functions ***) |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
485 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
486 |
(*Init HTML generator by setting paths and creating new files*) |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
487 |
fun init_html () = |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
488 |
let val cwd = OS.FileSys.getDir(); |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
489 |
val _ = mkdir (html_path cwd); |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
490 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
491 |
val theory_list = TextIO.closeOut (TextIO.openOut (tack_on (html_path cwd) "theory_list.txt")); |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
492 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
493 |
val rel_gif_path = relative_path (html_path cwd) (gif_path ()); |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
494 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
495 |
(*Make new HTML files for Pure and CPure*) |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
496 |
fun init_pure_html () = |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
497 |
let val pure_out = TextIO.openOut (tack_on (html_path cwd) "Pure_sub.html"); |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
498 |
val cpure_out = TextIO.openOut (tack_on (html_path cwd) "CPure_sub.html"); |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
499 |
in mk_charthead pure_out "Pure" "Children" false rel_gif_path "" |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
500 |
(!package); |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
501 |
mk_charthead cpure_out "CPure" "Children" false rel_gif_path "" |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
502 |
(!package); |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
503 |
TextIO.output (pure_out, "Pure\n"); |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
504 |
TextIO.output (cpure_out, "CPure\n"); |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
505 |
TextIO.closeOut pure_out; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
506 |
TextIO.closeOut cpure_out; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
507 |
pure_subchart := Some (html_path cwd) |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
508 |
end; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
509 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
510 |
in make_html := true; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
511 |
(*Make sure that base_path contains the physical path and no |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
512 |
symbolic links*) |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
513 |
base_path := normalize_path (!base_path); |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
514 |
original_path := cwd; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
515 |
index_path := html_path cwd; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
516 |
package := |
4215
7f7519759b8c
moved old file stuff from library.ML to Thy/browser_info.ML;
wenzelm
parents:
3976
diff
changeset
|
517 |
(if subdir_of (cwd, !base_path) then |
3603
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
518 |
relative_path (!base_path) cwd |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
519 |
else base_name cwd); |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
520 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
521 |
|
4215
7f7519759b8c
moved old file stuff from library.ML to Thy/browser_info.ML;
wenzelm
parents:
3976
diff
changeset
|
522 |
(*copy README files to html directory*) (* FIXME let usedir do this job !?*) |
7f7519759b8c
moved old file stuff from library.ML to Thy/browser_info.ML;
wenzelm
parents:
3976
diff
changeset
|
523 |
handle_error |
7f7519759b8c
moved old file stuff from library.ML to Thy/browser_info.ML;
wenzelm
parents:
3976
diff
changeset
|
524 |
(File.copy (tack_on cwd "README.html")) (tack_on (!index_path) "README.html"); |
7f7519759b8c
moved old file stuff from library.ML to Thy/browser_info.ML;
wenzelm
parents:
3976
diff
changeset
|
525 |
handle_error |
7f7519759b8c
moved old file stuff from library.ML to Thy/browser_info.ML;
wenzelm
parents:
3976
diff
changeset
|
526 |
(File.copy (tack_on cwd "README")) (tack_on (!index_path) "README"); |
7f7519759b8c
moved old file stuff from library.ML to Thy/browser_info.ML;
wenzelm
parents:
3976
diff
changeset
|
527 |
|
7f7519759b8c
moved old file stuff from library.ML to Thy/browser_info.ML;
wenzelm
parents:
3976
diff
changeset
|
528 |
if subdir_of (cwd, !base_path) then () |
3603
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
529 |
else warning "The current working directory seems to be no \ |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
530 |
\subdirectory of\nIsabelle's main directory. \ |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
531 |
\Please ensure that base_path's value is correct.\n"; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
532 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
533 |
writeln ("Setting path for index.html to " ^ quote (!index_path) ^ |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
534 |
"\nGIF path has been set to " ^ quote (gif_path ())); |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
535 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
536 |
if is_none (!pure_subchart) then init_pure_html() |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
537 |
else () |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
538 |
end; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
539 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
540 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
541 |
(*Generate index.html*) |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
542 |
fun finish_html () = if not (!make_html) then () else |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
543 |
let val tlist_path = tack_on (!index_path) "theory_list.txt"; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
544 |
val theory_list = TextIO.openIn tlist_path; |
3834 | 545 |
val theories = BAD_space_explode "\n" (TextIO.inputAll theory_list); |
3603
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
546 |
val dummy = (TextIO.closeIn theory_list; OS.FileSys.remove tlist_path); |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
547 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
548 |
val rel_gif_path = relative_path (!index_path) (gif_path ()); |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
549 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
550 |
(*Make entry for main chart of all theories.*) |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
551 |
fun main_entry t = |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
552 |
let |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
553 |
val (name, path) = take_prefix (not_equal " ") (explode t); |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
554 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
555 |
val tname = implode name |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
556 |
val tpath = tack_on (relative_path (!index_path) (html_path (implode (tl path)))) |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
557 |
tname; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
558 |
in "<A HREF = \"" ^ tpath ^ "_sub.html\"><IMG SRC = \"" ^ |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
559 |
tack_on rel_gif_path "red_arrow.gif\" BORDER=0 ALT = \\/></A>" ^ |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
560 |
"<A HREF = \"" ^ tpath ^ "_sup.html\"><IMG SRC = \"" ^ |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
561 |
tack_on rel_gif_path "blue_arrow.gif\ |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
562 |
\\" BORDER=0 ALT = /\\></A> <A HREF = \"" ^ tpath ^ |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
563 |
".html\">" ^ tname ^ "</A><BR>\n" |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
564 |
end; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
565 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
566 |
val out = TextIO.openOut (tack_on (!index_path) "index.html"); |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
567 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
568 |
(*Find out in which subdirectory of Isabelle's main directory the |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
569 |
index.html is placed; if original_path is no subdirectory of base_path |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
570 |
then take the last directory of index_path*) |
4215
7f7519759b8c
moved old file stuff from library.ML to Thy/browser_info.ML;
wenzelm
parents:
3976
diff
changeset
|
571 |
val inside_isabelle = subdir_of (!original_path, !base_path); |
3603
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
572 |
val subdir = |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
573 |
if inside_isabelle then relative_path (html_path (!base_path)) (!index_path) |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
574 |
else base_name (!index_path); |
3834 | 575 |
val subdirs = BAD_space_explode "/" subdir; |
3603
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
576 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
577 |
(*Look for index.html in superdirectories; stop when Isabelle's |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
578 |
main directory is reached*) |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
579 |
fun find_super_index [] n = ("", n) |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
580 |
| find_super_index (p::ps) n = |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
581 |
let val index_path = "/" ^ space_implode "/" (rev ps); |
4215
7f7519759b8c
moved old file stuff from library.ML to Thy/browser_info.ML;
wenzelm
parents:
3976
diff
changeset
|
582 |
in if File.exists (index_path ^ "/index.html") then (index_path, n) |
3603
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
583 |
else if length subdirs - n > 0 then find_super_index ps (n+1) |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
584 |
else ("", n) |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
585 |
end; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
586 |
val (super_index, level_diff) = |
3834 | 587 |
find_super_index (rev (BAD_space_explode "/" (!index_path))) 1; |
3603
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
588 |
val level = length subdirs - level_diff; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
589 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
590 |
(*Add link to current directory to 'super' index.html*) |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
591 |
fun link_directory () = |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
592 |
let val old_index = TextIO.openIn (super_index ^ "/index.html"); |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
593 |
val content = rev (explode (TextIO.inputAll old_index)); |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
594 |
val dummy = TextIO.closeIn old_index; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
595 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
596 |
val out = TextIO.openAppend (super_index ^ "/index.html"); |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
597 |
val rel_path = space_implode "/" (drop (level, subdirs)); |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
598 |
in |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
599 |
TextIO.output (out, |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
600 |
(if nth_elem (3, content) <> "!" then "" |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
601 |
else "\n<HR><H3>Subdirectories:</H3>\n") ^ |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
602 |
"<H3><A HREF = \"" ^ rel_path ^ "/index.html\">" ^ rel_path ^ |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
603 |
"</A></H3>\n"); |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
604 |
TextIO.closeOut out |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
605 |
end; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
606 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
607 |
(*If original_path is no subdirectory of base_path then the title should |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
608 |
not contain the string "Isabelle/"*) |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
609 |
val title = (if inside_isabelle then "Isabelle/" else "") ^ subdir; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
610 |
val rel_graph_path = tack_on (relative_path (!index_path) (graph_path (!original_path))) |
3748
e5d2399a154f
Changed html data directory and names of graph files.
berghofe
parents:
3639
diff
changeset
|
611 |
"small.html" |
3603
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
612 |
in TextIO.output (out, |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
613 |
"<HTML><HEAD><TITLE>" ^ title ^ "</TITLE></HEAD>\n\ |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
614 |
\<BODY><H2>" ^ title ^ "</H2>\n\ |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
615 |
\The name of every theory is linked to its theory file<BR>\n\ |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
616 |
\<IMG SRC = \"" ^ tack_on rel_gif_path "red_arrow.gif\ |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
617 |
\\" ALT = \\/></A> stands for subtheories (child theories)<BR>\n\ |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
618 |
\<IMG SRC = \"" ^ tack_on rel_gif_path "blue_arrow.gif\ |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
619 |
\\" ALT = /\\></A> stands for supertheories (parent theories)<P>\n\ |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
620 |
\View <A HREF=\"" ^ rel_graph_path ^ "\">graph</A> of theories<P>\n" ^ |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
621 |
(if super_index = "" then "" else |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
622 |
("<A HREF = \"" ^ relative_path (!index_path) super_index ^ |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
623 |
"/index.html\">Back</A> to the index of " ^ |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
624 |
(if not inside_isabelle then |
3834 | 625 |
hd (tl (rev (BAD_space_explode "/" (!index_path)))) |
3603
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
626 |
else if level = 0 then "Isabelle logics" |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
627 |
else space_implode "/" (take (level, subdirs))))) ^ |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
628 |
"\n" ^ |
4215
7f7519759b8c
moved old file stuff from library.ML to Thy/browser_info.ML;
wenzelm
parents:
3976
diff
changeset
|
629 |
(if File.exists (tack_on (!index_path) "README.html") then |
3868 | 630 |
"<BR>View the <A HREF = \"README.html\">README</A> file.\n" |
4215
7f7519759b8c
moved old file stuff from library.ML to Thy/browser_info.ML;
wenzelm
parents:
3976
diff
changeset
|
631 |
else if File.exists (tack_on (!index_path) "README") then |
3868 | 632 |
"<BR>View the <A HREF = \"README\">README</A> file.\n" |
3603
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
633 |
else "") ^ |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
634 |
"<HR>" ^ implode (map main_entry theories) ^ "<!-->"); |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
635 |
TextIO.closeOut out; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
636 |
if super_index = "" orelse (inside_isabelle andalso level = 0) then () |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
637 |
else link_directory () |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
638 |
end; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
639 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
640 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
641 |
(*Append section heading to HTML file*) |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
642 |
fun section s = |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
643 |
case !cur_htmlfile of |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
644 |
Some out => (mk_theorems_title out; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
645 |
TextIO.output (out, "<H3>" ^ s ^ "</H3>\n")) |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
646 |
| None => (); |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
647 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
648 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
649 |
(*Add theorem to HTML file*) |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
650 |
fun thm_to_html thm name = |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
651 |
case !cur_htmlfile of |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
652 |
Some out => |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
653 |
(mk_theorems_title out; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
654 |
TextIO.output (out, "<DD><EM>" ^ name ^ "</EM>\n<PRE>" ^ |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
655 |
(implode o escape) |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
656 |
(explode |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
657 |
(string_of_thm (#1 (freeze_thaw thm)))) ^ |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
658 |
"</PRE><P>\n") |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
659 |
) |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
660 |
| None => (); |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
661 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
662 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
663 |
(*Close HTML file*) |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
664 |
fun close_html () = |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
665 |
case !cur_htmlfile of |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
666 |
Some out => (TextIO.output (out, "<HR></BODY></HTML>\n"); |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
667 |
TextIO.closeOut out; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
668 |
cur_htmlfile := None) |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
669 |
| None => () ; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
670 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
671 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
672 |
(******************** Graph generation functions ************************) |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
673 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
674 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
675 |
(*flag that indicates whether graph files should be generated*) |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
676 |
val make_graph = ref false; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
677 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
678 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
679 |
(*file to use as basis for new graph files*) |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
680 |
val graph_base_file = ref ""; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
681 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
682 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
683 |
(*directory containing basic theories (gets label "base")*) |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
684 |
val graph_root_dir = ref ""; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
685 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
686 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
687 |
(*name of current graph file*) |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
688 |
val graph_file = ref ""; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
689 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
690 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
691 |
(*name of large graph file which also contains |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
692 |
theories defined in subdirectories *) |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
693 |
val large_graph_file = ref ""; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
694 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
695 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
696 |
(* initialize graph data generator *) |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
697 |
fun init_graph usedir_arg = |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
698 |
let |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
699 |
(*create default graph containing only Pure, CPure and ProtoPure*) |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
700 |
fun default_graph outfile = |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
701 |
let val os = TextIO.openOut outfile; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
702 |
in (TextIO.output(os,"\"ProtoPure\" \"ProtoPure\" \"Pure\" \"\" ;\n\ |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
703 |
\\"CPure\" \"CPure\" \"Pure\" \"\" > \"ProtoPure\" ;\n\ |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
704 |
\\"Pure\" \"Pure\" \"Pure\" \"\" > \"ProtoPure\" ;\n"); |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
705 |
TextIO.closeOut os) |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
706 |
end; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
707 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
708 |
(*copy graph file, adjust relative paths for theory files*) |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
709 |
fun copy_graph infile outfile unfold = |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
710 |
let val is = TextIO.openIn infile; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
711 |
val (inp_dir, _) = split_filename infile; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
712 |
val (outp_dir, _) = split_filename outfile; |
3834 | 713 |
val entries = map (BAD_space_explode " ") |
714 |
(BAD_space_explode "\n" (TextIO.inputAll is)); |
|
3603
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
715 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
716 |
fun thyfile f = if f = "\"\"" then f else |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
717 |
let val (dir, name) = |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
718 |
split_filename (implode (rev (tl (rev (tl (explode f)))))); |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
719 |
val abs_path = normalize_path (tack_on inp_dir dir); |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
720 |
val rel_path = tack_on (relative_path outp_dir abs_path) name |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
721 |
in quote rel_path end; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
722 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
723 |
fun process_entry (a::b::c::d::e::r) = |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
724 |
if d = "+" then |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
725 |
a::b::c::((if unfold then "+ " else "") ^ (thyfile e))::r |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
726 |
else |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
727 |
a::b::c::(thyfile d)::e::r; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
728 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
729 |
val _ = TextIO.closeIn is; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
730 |
val os = TextIO.openOut outfile; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
731 |
val _ = TextIO.output(os, (cat_lines |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
732 |
(map ((space_implode " ") o process_entry) entries)) ^ "\n"); |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
733 |
val _ = TextIO.closeOut os; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
734 |
in () end; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
735 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
736 |
(*create html page which contains graph browser applet*) |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
737 |
fun mk_applet_page abs_path large other_graph = |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
738 |
let |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
739 |
val dir_name = |
4215
7f7519759b8c
moved old file stuff from library.ML to Thy/browser_info.ML;
wenzelm
parents:
3976
diff
changeset
|
740 |
(if subdir_of (!original_path, !base_path) then "Isabelle/" else "") ^ |
3603
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
741 |
(relative_path (normalize_path (tack_on (!graph_root_dir) "..")) (pwd ())); |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
742 |
val rel_codebase = |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
743 |
relative_path abs_path (tack_on (normalize_path (!output_dir)) "graph"); |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
744 |
val rel_index_path = tack_on (relative_path |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
745 |
abs_path (tack_on (normalize_path (!output_dir)) "graph")) "index.html"; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
746 |
val outfile = |
3748
e5d2399a154f
Changed html data directory and names of graph files.
berghofe
parents:
3639
diff
changeset
|
747 |
tack_on abs_path ((if large then "large" else "small") ^ ".html"); |
3603
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
748 |
val os = TextIO.openOut outfile; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
749 |
val _ = TextIO.output(os, |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
750 |
"<HTML><HEAD><TITLE>" ^ dir_name ^ "</TITLE></HEAD>\n\ |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
751 |
\<BODY><H2>" ^ dir_name ^ "</H2>\n" ^ |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
752 |
(if other_graph then |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
753 |
(if large then |
3748
e5d2399a154f
Changed html data directory and names of graph files.
berghofe
parents:
3639
diff
changeset
|
754 |
"View <A HREF=\"small.html\">small graph</A> without \ |
3603
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
755 |
\subdirectories<P>\n" |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
756 |
else |
3748
e5d2399a154f
Changed html data directory and names of graph files.
berghofe
parents:
3639
diff
changeset
|
757 |
"View <A HREF=\"large.html\">large graph</A> including \ |
3603
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
758 |
\all subdirectories<P>\n") |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
759 |
else "") ^ |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
760 |
"<A HREF=\"" ^ rel_index_path ^ "\">Back</A> to index\n<HR>\n\ |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
761 |
\<APPLET CODE=\"GraphBrowser/GraphBrowser.class\" \ |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
762 |
\CODEBASE=\"" ^ rel_codebase ^ "\" WIDTH=550 HEIGHT=450>\n\ |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
763 |
\<PARAM NAME=\"graphfile\" VALUE=\"" ^ |
3748
e5d2399a154f
Changed html data directory and names of graph files.
berghofe
parents:
3639
diff
changeset
|
764 |
(if large then "large.graph" else "small.graph") ^ "\">\n\ |
3603
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
765 |
\</APPLET>\n<HR>\n</BODY></HTML>") |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
766 |
val _ = TextIO.closeOut os |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
767 |
in () end; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
768 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
769 |
val gpath = graph_path (pwd ()); |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
770 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
771 |
in |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
772 |
(make_graph := true; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
773 |
base_path := normalize_path (!base_path); |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
774 |
mkdir gpath; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
775 |
original_path := pwd (); |
3748
e5d2399a154f
Changed html data directory and names of graph files.
berghofe
parents:
3639
diff
changeset
|
776 |
graph_file := tack_on gpath "small.graph"; |
3603
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
777 |
graph_root_dir := (if usedir_arg = "." then pwd () |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
778 |
else normalize_path (tack_on (pwd ()) "..")); |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
779 |
(if (!graph_base_file) = "" then |
3748
e5d2399a154f
Changed html data directory and names of graph files.
berghofe
parents:
3639
diff
changeset
|
780 |
(large_graph_file := tack_on gpath "large.graph"; |
3603
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
781 |
default_graph (!graph_file); |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
782 |
default_graph (!large_graph_file); |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
783 |
mk_applet_page gpath false true; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
784 |
mk_applet_page gpath true true) |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
785 |
else |
4215
7f7519759b8c
moved old file stuff from library.ML to Thy/browser_info.ML;
wenzelm
parents:
3976
diff
changeset
|
786 |
(if subdir_of (fst (split_filename (!graph_file)), |
7f7519759b8c
moved old file stuff from library.ML to Thy/browser_info.ML;
wenzelm
parents:
3976
diff
changeset
|
787 |
(fst (split_filename (!graph_base_file)))) |
3603
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
788 |
then |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
789 |
(copy_graph (!graph_base_file) (!graph_file) true; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
790 |
mk_applet_page gpath false false) |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
791 |
else |
3748
e5d2399a154f
Changed html data directory and names of graph files.
berghofe
parents:
3639
diff
changeset
|
792 |
(large_graph_file := tack_on gpath "large.graph"; |
3603
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
793 |
mk_applet_page gpath false true; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
794 |
mk_applet_page gpath true true; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
795 |
copy_graph (!graph_base_file) (!graph_file) false; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
796 |
copy_graph (!graph_base_file) (!large_graph_file) false))); |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
797 |
graph_base_file := (!graph_file)) |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
798 |
end; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
799 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
800 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
801 |
(*add theory to graph definition file*) |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
802 |
fun mk_graph tname abs_path = if not (!make_graph) then () else |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
803 |
let val parents = |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
804 |
map (fn (t, _) => tack_on (path_of t) t) |
3976 | 805 |
(filter (fn (_, {children,...}) => tname mem children) |
3603
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
806 |
(Symtab.dest(!loaded_thys))); |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
807 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
808 |
val dir_name = relative_path |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
809 |
(normalize_path (tack_on (!graph_root_dir) "..")) abs_path; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
810 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
811 |
val dir_entry = "\"" ^ dir_name ^ |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
812 |
(if (tack_on abs_path "") = (tack_on (!graph_root_dir) "") |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
813 |
then "/base\" + " else "\" "); |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
814 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
815 |
val thy_file = (tack_on (html_path abs_path) tname) ^ ".html"; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
816 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
817 |
val thy_ID = quote (tack_on abs_path tname); |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
818 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
819 |
val entry_str_1 = (quote tname) ^ " " ^ thy_ID ^ " " ^ dir_entry ^ |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
820 |
(quote (relative_path (fst (split_filename (!graph_file))) thy_file)) ^ |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
821 |
" > " ^ (space_implode " " (map quote parents)) ^ " ;\n" ; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
822 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
823 |
val entry_str_2 = (quote tname) ^ " " ^ thy_ID ^ " " ^ dir_entry ^ |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
824 |
(quote (relative_path (fst (split_filename (!large_graph_file))) thy_file)) ^ |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
825 |
" > " ^ (space_implode " " (map quote parents)) ^ " ;\n" ; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
826 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
827 |
fun exists_entry id infile = |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
828 |
let val is = TextIO.openIn(infile); |
3834 | 829 |
val IDs = map (hd o tl o (BAD_space_explode " ")) |
830 |
(BAD_space_explode "\n" (TextIO.inputAll is)); |
|
3603
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
831 |
val _ = TextIO.closeIn is |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
832 |
in id mem IDs end; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
833 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
834 |
fun mk_entry outfile entry_str = |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
835 |
if exists_entry thy_ID outfile then () |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
836 |
else |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
837 |
let val os = TextIO.openAppend outfile; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
838 |
val _ = TextIO.output (os, entry_str); |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
839 |
val _ = TextIO.closeOut os; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
840 |
in () end |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
841 |
|
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
842 |
in (mk_entry (!graph_file) entry_str_1; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
843 |
mk_entry (!large_graph_file) entry_str_2) handle _ => |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
844 |
(make_graph:=false; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
845 |
warning ("Unable to write to graph file " ^ (!graph_file))) |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
846 |
end; |
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
847 |
|
4215
7f7519759b8c
moved old file stuff from library.ML to Thy/browser_info.ML;
wenzelm
parents:
3976
diff
changeset
|
848 |
|
3603
5eef2ff0eb72
This file now contains all functions for generating html
berghofe
parents:
diff
changeset
|
849 |
end; |