src/Pure/Thy/present.ML
author wenzelm
Wed, 22 Sep 2010 18:21:48 +0200
changeset 39616 8052101883c3
parent 38133 987680d2e77d
child 39733 6d373e9dcb9d
permissions -rw-r--r--
renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
6203
328b4377755c Theory presentation (fake implementation);
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/Thy/present.ML
9416
9144976964e7 removed all_sessions.graph;
wenzelm
parents: 9136
diff changeset
     2
    Author:     Markus Wenzel and Stefan Berghofer, TU Muenchen
6203
328b4377755c Theory presentation (fake implementation);
wenzelm
parents:
diff changeset
     3
9416
9144976964e7 removed all_sessions.graph;
wenzelm
parents: 9136
diff changeset
     4
Theory presentation: HTML, graph files, (PDF)LaTeX documents.
6203
328b4377755c Theory presentation (fake implementation);
wenzelm
parents:
diff changeset
     5
*)
328b4377755c Theory presentation (fake implementation);
wenzelm
parents:
diff changeset
     6
328b4377755c Theory presentation (fake implementation);
wenzelm
parents:
diff changeset
     7
signature BASIC_PRESENT =
328b4377755c Theory presentation (fake implementation);
wenzelm
parents:
diff changeset
     8
sig
11057
e68becb804fe added no_document
wenzelm
parents: 9917
diff changeset
     9
  val no_document: ('a -> 'b) -> 'a -> 'b
6203
328b4377755c Theory presentation (fake implementation);
wenzelm
parents:
diff changeset
    10
end;
328b4377755c Theory presentation (fake implementation);
wenzelm
parents:
diff changeset
    11
328b4377755c Theory presentation (fake implementation);
wenzelm
parents:
diff changeset
    12
signature PRESENT =
328b4377755c Theory presentation (fake implementation);
wenzelm
parents:
diff changeset
    13
sig
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
    14
  include BASIC_PRESENT
24561
7b4aa14d2491 tuned signature;
wenzelm
parents: 24150
diff changeset
    15
  val session_name: theory -> string
9452
fc02c5bacaab export write_graph;
wenzelm
parents: 9416
diff changeset
    16
  val write_graph: {name: string, ID: string, dir: string, unfold: bool,
fc02c5bacaab export write_graph;
wenzelm
parents: 9416
diff changeset
    17
   path: string, parents: string list} list -> Path.T -> unit
20577
a96883a6d709 added display_graph (from thm_deps.ML);
wenzelm
parents: 19305
diff changeset
    18
  val display_graph: {name: string, ID: string, dir: string, unfold: bool,
a96883a6d709 added display_graph (from thm_deps.ML);
wenzelm
parents: 19305
diff changeset
    19
   path: string, parents: string list} list -> unit
17082
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
    20
  val init: bool -> bool -> string -> bool -> string list -> string list ->
23899
ab37b1f690c7 clarified init/begin_theory: no longer depend on thy_info.ML;
wenzelm
parents: 23884
diff changeset
    21
    string -> (bool * Path.T) option -> Url.T option * bool -> bool -> theory list -> unit
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
    22
  val finish: unit -> unit
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
    23
  val init_theory: string -> unit
27862
8f727f7c8c1d removed obsolete verbatim_source, results, chapter, section etc.;
wenzelm
parents: 27491
diff changeset
    24
  val theory_source: string -> (unit -> HTML.text) -> unit
9136
8196955b02ec adapted to improved presentation;
wenzelm
parents: 9044
diff changeset
    25
  val theory_output: string -> string -> unit
24150
ed724867099a sort indexes according to symbolic update_time (multithreading-safe);
wenzelm
parents: 24102
diff changeset
    26
  val begin_theory: int -> Path.T -> (Path.T * bool) list -> theory -> theory
14922
88c1e108d0bf added Present.drafts;
wenzelm
parents: 14898
diff changeset
    27
  val drafts: string -> Path.T list -> Path.T
6203
328b4377755c Theory presentation (fake implementation);
wenzelm
parents:
diff changeset
    28
end;
328b4377755c Theory presentation (fake implementation);
wenzelm
parents:
diff changeset
    29
7685
3edd32d588a6 improved theory_source presentation (hook);
wenzelm
parents: 6325
diff changeset
    30
structure Present: PRESENT =
3edd32d588a6 improved theory_source presentation (hook);
wenzelm
parents: 6325
diff changeset
    31
struct
3edd32d588a6 improved theory_source presentation (hook);
wenzelm
parents: 6325
diff changeset
    32
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
    33
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
    34
(** paths **)
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
    35
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
    36
val output_path = Path.variable "ISABELLE_BROWSER_INFO";
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
    37
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
    38
val tex_ext = Path.ext "tex";
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
    39
val tex_path = tex_ext o Path.basic;
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
    40
val html_ext = Path.ext "html";
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
    41
val html_path = html_ext o Path.basic;
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
    42
val index_path = Path.basic "index.html";
11856
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
    43
val readme_html_path = Path.basic "README.html";
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
    44
val readme_path = Path.basic "README";
17082
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
    45
val documentN = "document";
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
    46
val document_path = Path.basic documentN;
8196
ecb9decd38ac additional tex dump;
wenzelm
parents: 8192
diff changeset
    47
val doc_indexN = "session";
11856
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
    48
val graph_path = Path.basic "session.graph";
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
    49
val graph_pdf_path = Path.basic "session_graph.pdf";
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
    50
val graph_eps_path = Path.basic "session_graph.eps";
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
    51
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
    52
val session_path = Path.basic ".session";
21858
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 20664
diff changeset
    53
val session_entries_path = Path.explode ".session/entries";
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 20664
diff changeset
    54
val pre_index_path = Path.explode ".session/pre-index";
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
    55
9044
28ee037278a6 Reorganized graph stuff.
berghofe
parents: 8808
diff changeset
    56
fun mk_rel_path [] ys = Path.make ys
28ee037278a6 Reorganized graph stuff.
berghofe
parents: 8808
diff changeset
    57
  | mk_rel_path xs [] = Path.appends (replicate (length xs) Path.parent)
9416
9144976964e7 removed all_sessions.graph;
wenzelm
parents: 9136
diff changeset
    58
  | mk_rel_path (ps as x :: xs) (qs as y :: ys) = if x = y then mk_rel_path xs ys else
9044
28ee037278a6 Reorganized graph stuff.
berghofe
parents: 8808
diff changeset
    59
      Path.appends (replicate (length ps) Path.parent @ [Path.make qs]);
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
    60
21858
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 20664
diff changeset
    61
fun show_path path = Path.implode (Path.append (File.pwd ()) path);
11856
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
    62
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
    63
14922
88c1e108d0bf added Present.drafts;
wenzelm
parents: 14898
diff changeset
    64
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
    65
(** additional theory data **)
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
    66
33522
737589bb9bb8 adapted Theory_Data;
wenzelm
parents: 32738
diff changeset
    67
structure BrowserInfoData = Theory_Data
22846
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22580
diff changeset
    68
(
9416
9144976964e7 removed all_sessions.graph;
wenzelm
parents: 9136
diff changeset
    69
  type T = {name: string, session: string list, is_local: bool};
27329
91c0c894e1b4 session name: empty for Pure and by default;
wenzelm
parents: 27327
diff changeset
    70
  val empty = {name = "", session = [], is_local = false}: T;
16503
24491bde68df clarify empty vs. pure browser info;
wenzelm
parents: 16426
diff changeset
    71
  fun extend _ = empty;
33522
737589bb9bb8 adapted Theory_Data;
wenzelm
parents: 32738
diff changeset
    72
  fun merge _ = empty;
22846
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22580
diff changeset
    73
);
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
    74
27327
efd626efcb04 info: default name is "", not "Pure";
wenzelm
parents: 26957
diff changeset
    75
val put_info = BrowserInfoData.put;
26957
e3f04fdd994d eliminated theory CPure;
wenzelm
parents: 26433
diff changeset
    76
val get_info = BrowserInfoData.get;
24561
7b4aa14d2491 tuned signature;
wenzelm
parents: 24150
diff changeset
    77
val session_name = #name o get_info;
7b4aa14d2491 tuned signature;
wenzelm
parents: 24150
diff changeset
    78
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
    79
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
    80
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
    81
(** graphs **)
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
    82
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
    83
type graph_node =
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
    84
  {name: string, ID: string, dir: string, unfold: bool,
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
    85
   path: string, parents: string list};
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
    86
9416
9144976964e7 removed all_sessions.graph;
wenzelm
parents: 9136
diff changeset
    87
fun write_graph gr path =
9144976964e7 removed all_sessions.graph;
wenzelm
parents: 9136
diff changeset
    88
  File.write path (cat_lines (map (fn {name, ID, dir, unfold, path, parents} =>
9144976964e7 removed all_sessions.graph;
wenzelm
parents: 9136
diff changeset
    89
    "\"" ^ name ^ "\" \"" ^ ID ^ "\" \"" ^ dir ^ (if unfold then "\" + \"" else "\" \"") ^
28840
wenzelm
parents: 28500
diff changeset
    90
    path ^ "\" > " ^ space_implode " " (map quote parents) ^ " ;") gr));
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
    91
20577
a96883a6d709 added display_graph (from thm_deps.ML);
wenzelm
parents: 19305
diff changeset
    92
fun display_graph gr =
a96883a6d709 added display_graph (from thm_deps.ML);
wenzelm
parents: 19305
diff changeset
    93
  let
24561
7b4aa14d2491 tuned signature;
wenzelm
parents: 24150
diff changeset
    94
    val _ = writeln "Displaying graph ...";
21858
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 20664
diff changeset
    95
    val path = File.tmp_path (Path.explode "tmp.graph");
20577
a96883a6d709 added display_graph (from thm_deps.ML);
wenzelm
parents: 19305
diff changeset
    96
    val _ = write_graph gr path;
31819
2c0ab4485f48 tune File.isabelle_tool signature;
wenzelm
parents: 29606
diff changeset
    97
    val _ = File.isabelle_tool "browser" ("-c " ^ File.shell_path path ^ " &");
20577
a96883a6d709 added display_graph (from thm_deps.ML);
wenzelm
parents: 19305
diff changeset
    98
  in () end;
a96883a6d709 added display_graph (from thm_deps.ML);
wenzelm
parents: 19305
diff changeset
    99
a96883a6d709 added display_graph (from thm_deps.ML);
wenzelm
parents: 19305
diff changeset
   100
9416
9144976964e7 removed all_sessions.graph;
wenzelm
parents: 9136
diff changeset
   101
fun ID_of sess s = space_implode "/" (sess @ [s]);
23899
ab37b1f690c7 clarified init/begin_theory: no longer depend on thy_info.ML;
wenzelm
parents: 23884
diff changeset
   102
fun ID_of_thy thy = ID_of (#session (get_info thy)) (Context.theory_name thy);
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   103
23899
ab37b1f690c7 clarified init/begin_theory: no longer depend on thy_info.ML;
wenzelm
parents: 23884
diff changeset
   104
ab37b1f690c7 clarified init/begin_theory: no longer depend on thy_info.ML;
wenzelm
parents: 23884
diff changeset
   105
(*retrieve graph data from initial collection of theories*)
24150
ed724867099a sort indexes according to symbolic update_time (multithreading-safe);
wenzelm
parents: 24102
diff changeset
   106
fun init_graph remote_path curr_sess = rev o map (fn thy =>
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   107
  let
23899
ab37b1f690c7 clarified init/begin_theory: no longer depend on thy_info.ML;
wenzelm
parents: 23884
diff changeset
   108
    val name = Context.theory_name thy;
ab37b1f690c7 clarified init/begin_theory: no longer depend on thy_info.ML;
wenzelm
parents: 23884
diff changeset
   109
    val {name = sess_name, session, is_local} = get_info thy;
9416
9144976964e7 removed all_sessions.graph;
wenzelm
parents: 9136
diff changeset
   110
    val path' = Path.append (Path.make session) (html_path name);
24150
ed724867099a sort indexes according to symbolic update_time (multithreading-safe);
wenzelm
parents: 24102
diff changeset
   111
    val entry =
ed724867099a sort indexes according to symbolic update_time (multithreading-safe);
wenzelm
parents: 24102
diff changeset
   112
     {name = name, ID = ID_of session name, dir = sess_name,
ed724867099a sort indexes according to symbolic update_time (multithreading-safe);
wenzelm
parents: 24102
diff changeset
   113
      path =
ed724867099a sort indexes according to symbolic update_time (multithreading-safe);
wenzelm
parents: 24102
diff changeset
   114
        if null session then "" else
ed724867099a sort indexes according to symbolic update_time (multithreading-safe);
wenzelm
parents: 24102
diff changeset
   115
        if is_some remote_path andalso not is_local then
ed724867099a sort indexes according to symbolic update_time (multithreading-safe);
wenzelm
parents: 24102
diff changeset
   116
          Url.implode (Url.append (the remote_path) (Url.File
ed724867099a sort indexes according to symbolic update_time (multithreading-safe);
wenzelm
parents: 24102
diff changeset
   117
            (Path.append (Path.make session) (html_path name))))
ed724867099a sort indexes according to symbolic update_time (multithreading-safe);
wenzelm
parents: 24102
diff changeset
   118
        else Path.implode (Path.append (mk_rel_path curr_sess session) (html_path name)),
ed724867099a sort indexes according to symbolic update_time (multithreading-safe);
wenzelm
parents: 24102
diff changeset
   119
      unfold = false,
ed724867099a sort indexes according to symbolic update_time (multithreading-safe);
wenzelm
parents: 24102
diff changeset
   120
      parents = map ID_of_thy (Theory.parents_of thy)};
ed724867099a sort indexes according to symbolic update_time (multithreading-safe);
wenzelm
parents: 24102
diff changeset
   121
  in (0, entry) end);
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   122
24150
ed724867099a sort indexes according to symbolic update_time (multithreading-safe);
wenzelm
parents: 24102
diff changeset
   123
fun ins_graph_entry (i, entry as {ID, ...}) (gr: (int * graph_node) list) =
ed724867099a sort indexes according to symbolic update_time (multithreading-safe);
wenzelm
parents: 24102
diff changeset
   124
  (i, entry) :: filter_out (fn (_, entry') => #ID entry' = ID) gr;
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   125
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   126
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   127
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   128
(** global browser info state **)
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   129
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   130
(* type theory_info *)
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   131
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   132
type theory_info = {tex_source: Buffer.T, html_source: Buffer.T, html: Buffer.T};
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   133
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   134
fun make_theory_info (tex_source, html_source, html) =
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   135
  {tex_source = tex_source, html_source = html_source, html = html}: theory_info;
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   136
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   137
val empty_theory_info = make_theory_info (Buffer.empty, Buffer.empty, Buffer.empty);
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   138
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   139
fun map_theory_info f {tex_source, html_source, html} =
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   140
  make_theory_info (f (tex_source, html_source, html));
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   141
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   142
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   143
(* type browser_info *)
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   144
11856
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
   145
type browser_info = {theories: theory_info Symtab.table, files: (Path.T * string) list,
24150
ed724867099a sort indexes according to symbolic update_time (multithreading-safe);
wenzelm
parents: 24102
diff changeset
   146
  tex_index: (int * string) list, html_index: (int * string) list, graph: (int * graph_node) list};
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   147
11856
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
   148
fun make_browser_info (theories, files, tex_index, html_index, graph) =
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
   149
  {theories = theories, files = files, tex_index = tex_index, html_index = html_index,
9416
9144976964e7 removed all_sessions.graph;
wenzelm
parents: 9136
diff changeset
   150
    graph = graph}: browser_info;
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   151
24150
ed724867099a sort indexes according to symbolic update_time (multithreading-safe);
wenzelm
parents: 24102
diff changeset
   152
val empty_browser_info = make_browser_info (Symtab.empty, [], [], [], []);
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   153
23899
ab37b1f690c7 clarified init/begin_theory: no longer depend on thy_info.ML;
wenzelm
parents: 23884
diff changeset
   154
fun init_browser_info remote_path curr_sess thys = make_browser_info
24150
ed724867099a sort indexes according to symbolic update_time (multithreading-safe);
wenzelm
parents: 24102
diff changeset
   155
  (Symtab.empty, [], [], [], init_graph remote_path curr_sess thys);
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   156
11856
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
   157
fun map_browser_info f {theories, files, tex_index, html_index, graph} =
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
   158
  make_browser_info (f (theories, files, tex_index, html_index, graph));
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   159
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   160
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   161
(* state *)
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   162
32738
15bb09ca0378 explicit indication of Unsynchronized.ref;
wenzelm
parents: 31819
diff changeset
   163
val browser_info = Unsynchronized.ref empty_browser_info;
15bb09ca0378 explicit indication of Unsynchronized.ref;
wenzelm
parents: 31819
diff changeset
   164
fun change_browser_info f =
15bb09ca0378 explicit indication of Unsynchronized.ref;
wenzelm
parents: 31819
diff changeset
   165
  CRITICAL (fn () => Unsynchronized.change browser_info (map_browser_info f));
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   166
32738
15bb09ca0378 explicit indication of Unsynchronized.ref;
wenzelm
parents: 31819
diff changeset
   167
val suppress_tex_source = Unsynchronized.ref false;
39616
8052101883c3 renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
wenzelm
parents: 38133
diff changeset
   168
fun no_document f x = Unsynchronized.setmp suppress_tex_source true f x;  (* FIXME unreliable *)
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   169
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   170
fun init_theory_info name info =
11856
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
   171
  change_browser_info (fn (theories, files, tex_index, html_index, graph) =>
17412
e26cb20ef0cc TableFun/Symtab: curried lookup and update;
wenzelm
parents: 17221
diff changeset
   172
    (Symtab.update (name, info) theories, files, tex_index, html_index, graph));
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   173
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   174
fun change_theory_info name f =
11856
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
   175
  change_browser_info (fn (info as (theories, files, tex_index, html_index, graph)) =>
17412
e26cb20ef0cc TableFun/Symtab: curried lookup and update;
wenzelm
parents: 17221
diff changeset
   176
    (case Symtab.lookup theories name of
27491
c8178a6a6480 begin_theory: files_html needs to be produced outside of prep_html_source to make ML files appear!
wenzelm
parents: 27329
diff changeset
   177
      NONE => error ("Browser info: cannot access theory document " ^ quote name)
17412
e26cb20ef0cc TableFun/Symtab: curried lookup and update;
wenzelm
parents: 17221
diff changeset
   178
    | SOME info => (Symtab.update (name, map_theory_info f info) theories, files,
9416
9144976964e7 removed all_sessions.graph;
wenzelm
parents: 9136
diff changeset
   179
        tex_index, html_index, graph)));
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   180
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   181
11856
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
   182
fun add_file file =
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
   183
  change_browser_info (fn (theories, files, tex_index, html_index, graph) =>
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
   184
    (theories, file :: files, tex_index, html_index, graph));
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
   185
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   186
fun add_tex_index txt =
11856
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
   187
  change_browser_info (fn (theories, files, tex_index, html_index, graph) =>
24150
ed724867099a sort indexes according to symbolic update_time (multithreading-safe);
wenzelm
parents: 24102
diff changeset
   188
    (theories, files, txt :: tex_index, html_index, graph));
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   189
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   190
fun add_html_index txt =
11856
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
   191
  change_browser_info (fn (theories, files, tex_index, html_index, graph) =>
24150
ed724867099a sort indexes according to symbolic update_time (multithreading-safe);
wenzelm
parents: 24102
diff changeset
   192
    (theories, files, tex_index, txt :: html_index, graph));
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   193
24150
ed724867099a sort indexes according to symbolic update_time (multithreading-safe);
wenzelm
parents: 24102
diff changeset
   194
fun add_graph_entry entry =
11856
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
   195
  change_browser_info (fn (theories, files, tex_index, html_index, graph) =>
24150
ed724867099a sort indexes according to symbolic update_time (multithreading-safe);
wenzelm
parents: 24102
diff changeset
   196
    (theories, files, tex_index, html_index, ins_graph_entry entry graph));
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   197
11057
e68becb804fe added no_document
wenzelm
parents: 9917
diff changeset
   198
fun add_tex_source name txt =
e68becb804fe added no_document
wenzelm
parents: 9917
diff changeset
   199
  if ! suppress_tex_source then ()
e68becb804fe added no_document
wenzelm
parents: 9917
diff changeset
   200
  else change_theory_info name (fn (tex_source, html_source, html) =>
e68becb804fe added no_document
wenzelm
parents: 9917
diff changeset
   201
    (Buffer.add txt tex_source, html_source, html));
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   202
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   203
fun add_html_source name txt = change_theory_info name (fn (tex_source, html_source, html) =>
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   204
  (tex_source, Buffer.add txt html_source, html));
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   205
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   206
fun add_html name txt = change_theory_info name (fn (tex_source, html_source, html) =>
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   207
  (tex_source, html_source, Buffer.add txt html));
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   208
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   209
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   210
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   211
(** global session state **)
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   212
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   213
(* session_info *)
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   214
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   215
type session_info =
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   216
  {name: string, parent: string, session: string, path: string list, html_prefix: Path.T,
17082
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   217
    info: bool, doc_format: string, doc_graph: bool, documents: (string * string) list,
17210
e80fd664a119 added copy-dump option;
wenzelm
parents: 17177
diff changeset
   218
    doc_prefix1: (Path.T * Path.T) option, doc_prefix2: (bool * Path.T) option,
e80fd664a119 added copy-dump option;
wenzelm
parents: 17177
diff changeset
   219
    remote_path: Url.T option, verbose: bool, readme: Path.T option};
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   220
9416
9144976964e7 removed all_sessions.graph;
wenzelm
parents: 9136
diff changeset
   221
fun make_session_info
17082
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   222
  (name, parent, session, path, html_prefix, info, doc_format, doc_graph, documents,
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   223
    doc_prefix1, doc_prefix2, remote_path, verbose, readme) =
7802
fba7a36e8556 isatool_document;
wenzelm
parents: 7789
diff changeset
   224
  {name = name, parent = parent, session = session, path = path, html_prefix = html_prefix,
17082
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   225
    info = info, doc_format = doc_format, doc_graph = doc_graph, documents = documents,
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   226
    doc_prefix1 = doc_prefix1, doc_prefix2 = doc_prefix2, remote_path = remote_path,
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   227
    verbose = verbose, readme = readme}: session_info;
7685
3edd32d588a6 improved theory_source presentation (hook);
wenzelm
parents: 6325
diff changeset
   228
3edd32d588a6 improved theory_source presentation (hook);
wenzelm
parents: 6325
diff changeset
   229
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   230
(* state *)
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   231
32738
15bb09ca0378 explicit indication of Unsynchronized.ref;
wenzelm
parents: 31819
diff changeset
   232
val session_info = Unsynchronized.ref (NONE: session_info option);
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   233
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15159
diff changeset
   234
fun with_session x f = (case ! session_info of NONE => x | SOME info => f info);
26433
9c2cdf28ecec eliminated theory ProtoPure;
wenzelm
parents: 26323
diff changeset
   235
fun with_context f = f (Context.theory_name (ML_Context.the_global_context ()));
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   236
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   237
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   238
14922
88c1e108d0bf added Present.drafts;
wenzelm
parents: 14898
diff changeset
   239
(** document preparation **)
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   240
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   241
(* maintain index *)
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   242
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   243
val session_entries =
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   244
  HTML.session_entries o
14898
a25550451b51 Url.File;
wenzelm
parents: 14598
diff changeset
   245
    map (fn name => (Url.File (Path.append (Path.basic name) index_path), name));
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   246
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   247
fun get_entries dir =
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   248
  split_lines (File.read (Path.append dir session_entries_path));
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   249
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   250
fun put_entries entries dir =
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   251
  File.write (Path.append dir session_entries_path) (cat_lines entries);
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   252
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   253
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   254
fun create_index dir =
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   255
  File.read (Path.append dir pre_index_path) ^
27862
8f727f7c8c1d removed obsolete verbatim_source, results, chapter, section etc.;
wenzelm
parents: 27491
diff changeset
   256
    session_entries (get_entries dir) ^ HTML.end_document
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   257
  |> File.write (Path.append dir index_path);
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   258
24150
ed724867099a sort indexes according to symbolic update_time (multithreading-safe);
wenzelm
parents: 24102
diff changeset
   259
fun update_index dir name = CRITICAL (fn () =>
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   260
  (case try get_entries dir of
21858
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 20664
diff changeset
   261
    NONE => warning ("Browser info: cannot access session index of " ^ quote (Path.implode dir))
24150
ed724867099a sort indexes according to symbolic update_time (multithreading-safe);
wenzelm
parents: 24102
diff changeset
   262
  | SOME es => (put_entries ((remove (op =) name es) @ [name]) dir; create_index dir)));
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   263
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   264
17082
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   265
(* document versions *)
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   266
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   267
fun read_version str =
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   268
  (case space_explode "=" str of
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   269
    [name] => (name, "")
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   270
  | [name, tags] => (name, tags)
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   271
  | _ => error ("Malformed document version specification: " ^ quote str));
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   272
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   273
fun read_versions strs =
19046
bc5c6c9b114e removed distinct, renamed gen_distinct to distinct;
wenzelm
parents: 18708
diff changeset
   274
  rev (distinct (eq_fst (op =)) (rev ((documentN, "") :: map read_version strs)))
28375
c879d88d038a eliminated polymorphic equality;
wenzelm
parents: 28027
diff changeset
   275
  |> filter_out (fn (_, s) => s = "-");
17082
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   276
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   277
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   278
(* init session *)
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   279
12895
d9dd528ecea6 clarified copy_all;
wenzelm
parents: 12849
diff changeset
   280
fun name_of_session elems = space_implode "/" ("Isabelle" :: elems);
d9dd528ecea6 clarified copy_all;
wenzelm
parents: 12849
diff changeset
   281
17082
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   282
fun init build info doc doc_graph doc_versions path name doc_prefix2
23944
2ea068548a83 marked some CRITICAL sections;
wenzelm
parents: 23899
diff changeset
   283
    (remote_path, first_time) verbose thys = CRITICAL (fn () =>
11911
6533ceee4cd7 build option enables most basic browser info (for proper recording of session);
wenzelm
parents: 11856
diff changeset
   284
  if not build andalso not info andalso doc = "" andalso is_none doc_prefix2 then
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15159
diff changeset
   285
    (browser_info := empty_browser_info; session_info := NONE)
11856
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
   286
  else
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
   287
    let
33957
e9afca2118d4 normalized uncurry take/drop
haftmann
parents: 33955
diff changeset
   288
      val parent_name = name_of_session (take (length path - 1) path);
11856
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
   289
      val session_name = name_of_session path;
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
   290
      val sess_prefix = Path.make path;
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
   291
      val html_prefix = Path.append (Path.expand output_path) sess_prefix;
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   292
17082
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   293
      val (doc_prefix1, documents) =
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   294
        if doc = "" then (NONE, [])
21962
279b129498b6 removed conditional combinator;
wenzelm
parents: 21858
diff changeset
   295
        else if not (File.exists document_path) then
22580
d91b4dd651d6 cleaned-up Output functions;
wenzelm
parents: 22123
diff changeset
   296
          (if verbose then Output.std_error "Warning: missing document directory\n" else ();
d91b4dd651d6 cleaned-up Output functions;
wenzelm
parents: 22123
diff changeset
   297
            (NONE, []))
17082
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   298
        else (SOME (Path.append html_prefix document_path, html_prefix),
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   299
          read_versions doc_versions);
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   300
11856
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
   301
      val parent_index_path = Path.append Path.parent index_path;
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
   302
      val index_up_lnk = if first_time then
16263
0609fb8df4a7 removed copy, copy_all (superceded by File.copy, File.copy_dir);
wenzelm
parents: 15801
diff changeset
   303
          Url.append (the remote_path) (Url.File (Path.append sess_prefix parent_index_path))
14898
a25550451b51 Url.File;
wenzelm
parents: 14598
diff changeset
   304
        else Url.File parent_index_path;
11856
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
   305
      val readme =
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15159
diff changeset
   306
        if File.exists readme_html_path then SOME readme_html_path
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15159
diff changeset
   307
        else if File.exists readme_path then SOME readme_path
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15159
diff changeset
   308
        else NONE;
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   309
17082
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   310
      val docs =
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   311
        (case readme of NONE => [] | SOME p => [(Url.File p, "README")]) @
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   312
        map (fn (name, _) => (Url.File (Path.ext doc (Path.basic name)), name)) documents;
11856
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
   313
      val index_text = HTML.begin_index (index_up_lnk, parent_name)
21858
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 20664
diff changeset
   314
        (Url.File index_path, session_name) docs (Url.explode "medium.html");
11856
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
   315
    in
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15159
diff changeset
   316
      session_info := SOME (make_session_info (name, parent_name, session_name, path, html_prefix,
17082
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   317
      info, doc, doc_graph, documents, doc_prefix1, doc_prefix2, remote_path, verbose, readme));
23899
ab37b1f690c7 clarified init/begin_theory: no longer depend on thy_info.ML;
wenzelm
parents: 23884
diff changeset
   318
      browser_info := init_browser_info remote_path path thys;
24150
ed724867099a sort indexes according to symbolic update_time (multithreading-safe);
wenzelm
parents: 24102
diff changeset
   319
      add_html_index (0, index_text)
23944
2ea068548a83 marked some CRITICAL sections;
wenzelm
parents: 23899
diff changeset
   320
    end);
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   321
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   322
28496
4cff10648928 renamed isatool to isabelle_tool in programming interfaces;
wenzelm
parents: 28375
diff changeset
   323
(* isabelle tool wrappers *)
17082
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   324
28496
4cff10648928 renamed isatool to isabelle_tool in programming interfaces;
wenzelm
parents: 28375
diff changeset
   325
fun isabelle_document verbose format name tags path result_path =
17082
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   326
  let
28500
4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL;
wenzelm
parents: 28496
diff changeset
   327
    val s = "\"$ISABELLE_TOOL\" document -c -o '" ^ format ^ "' \
33682
0c5d1485dea7 isabelle_document: more explicit error output, notably for drafts;
wenzelm
parents: 33522
diff changeset
   328
      \-n '" ^ name ^ "' -t '" ^ tags ^ "' " ^ File.shell_path path ^ " 2>&1";
17082
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   329
    val doc_path = Path.append result_path (Path.ext format (Path.basic name));
33682
0c5d1485dea7 isabelle_document: more explicit error output, notably for drafts;
wenzelm
parents: 33522
diff changeset
   330
    val _ = if verbose then writeln s else ();
35010
d6e492cea6e4 renamed system/system_out to bash/bash_output -- to emphasized that this is really GNU bash, not some undefined POSIX sh;
wenzelm
parents: 33957
diff changeset
   331
    val (out, rc) = bash_output s;
33682
0c5d1485dea7 isabelle_document: more explicit error output, notably for drafts;
wenzelm
parents: 33522
diff changeset
   332
    val _ =
0c5d1485dea7 isabelle_document: more explicit error output, notably for drafts;
wenzelm
parents: 33522
diff changeset
   333
      if not (File.exists doc_path) orelse rc <> 0 then
0c5d1485dea7 isabelle_document: more explicit error output, notably for drafts;
wenzelm
parents: 33522
diff changeset
   334
        cat_error out ("Failed to build document " ^ quote (show_path doc_path))
0c5d1485dea7 isabelle_document: more explicit error output, notably for drafts;
wenzelm
parents: 33522
diff changeset
   335
      else if verbose then writeln out
0c5d1485dea7 isabelle_document: more explicit error output, notably for drafts;
wenzelm
parents: 33522
diff changeset
   336
      else ();
0c5d1485dea7 isabelle_document: more explicit error output, notably for drafts;
wenzelm
parents: 33522
diff changeset
   337
  in doc_path end;
17082
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   338
28496
4cff10648928 renamed isatool to isabelle_tool in programming interfaces;
wenzelm
parents: 28375
diff changeset
   339
fun isabelle_browser graph =
17082
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   340
  let
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   341
    val pdf_path = File.tmp_path graph_pdf_path;
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   342
    val eps_path = File.tmp_path graph_eps_path;
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   343
    val gr_path = File.tmp_path graph_path;
31819
2c0ab4485f48 tune File.isabelle_tool signature;
wenzelm
parents: 29606
diff changeset
   344
    val args = "-o " ^ File.shell_path pdf_path ^ " " ^ File.shell_path gr_path;
17082
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   345
  in
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   346
    write_graph graph gr_path;
31819
2c0ab4485f48 tune File.isabelle_tool signature;
wenzelm
parents: 29606
diff changeset
   347
    if File.isabelle_tool "browser" args <> 0 orelse
2c0ab4485f48 tune File.isabelle_tool signature;
wenzelm
parents: 29606
diff changeset
   348
      not (File.exists eps_path) orelse not (File.exists pdf_path)
17082
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   349
    then error "Failed to prepare dependency graph"
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   350
    else
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   351
      let val pdf = File.read pdf_path and eps = File.read eps_path
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   352
      in File.rm pdf_path; File.rm eps_path; File.rm gr_path; (pdf, eps) end
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   353
  end;
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   354
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   355
11856
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
   356
(* finish session -- output all generated text *)
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
   357
24150
ed724867099a sort indexes according to symbolic update_time (multithreading-safe);
wenzelm
parents: 24102
diff changeset
   358
fun sorted_index index = map snd (sort (int_ord o pairself fst) (rev index));
ed724867099a sort indexes according to symbolic update_time (multithreading-safe);
wenzelm
parents: 24102
diff changeset
   359
fun index_buffer index = Buffer.add (implode (sorted_index index)) Buffer.empty;
ed724867099a sort indexes according to symbolic update_time (multithreading-safe);
wenzelm
parents: 24102
diff changeset
   360
14922
88c1e108d0bf added Present.drafts;
wenzelm
parents: 14898
diff changeset
   361
fun write_tex src name path =
28027
051d5ccbafc5 renamed Buffer.write to File.write_buffer;
wenzelm
parents: 27862
diff changeset
   362
  File.write_buffer (Path.append path (tex_path name)) src;
14922
88c1e108d0bf added Present.drafts;
wenzelm
parents: 14898
diff changeset
   363
88c1e108d0bf added Present.drafts;
wenzelm
parents: 14898
diff changeset
   364
fun write_tex_index tex_index path =
24150
ed724867099a sort indexes according to symbolic update_time (multithreading-safe);
wenzelm
parents: 24102
diff changeset
   365
  write_tex (index_buffer tex_index |> Buffer.add Latex.tex_trailer) doc_indexN path;
14922
88c1e108d0bf added Present.drafts;
wenzelm
parents: 14898
diff changeset
   366
7685
3edd32d588a6 improved theory_source presentation (hook);
wenzelm
parents: 6325
diff changeset
   367
23944
2ea068548a83 marked some CRITICAL sections;
wenzelm
parents: 23899
diff changeset
   368
fun finish () = CRITICAL (fn () =>
2ea068548a83 marked some CRITICAL sections;
wenzelm
parents: 23899
diff changeset
   369
    with_session () (fn {name, info, html_prefix, doc_format, doc_graph,
2ea068548a83 marked some CRITICAL sections;
wenzelm
parents: 23899
diff changeset
   370
      documents, doc_prefix1, doc_prefix2, path, verbose, readme, ...} =>
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   371
  let
11856
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
   372
    val {theories, files, tex_index, html_index, graph} = ! browser_info;
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
   373
    val thys = Symtab.dest theories;
9416
9144976964e7 removed all_sessions.graph;
wenzelm
parents: 9136
diff changeset
   374
    val parent_html_prefix = Path.append html_prefix Path.parent;
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   375
11856
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
   376
    fun finish_tex path (a, {tex_source, ...}: theory_info) = write_tex tex_source a path;
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
   377
    fun finish_html (a, {html, ...}: theory_info) =
28027
051d5ccbafc5 renamed Buffer.write to File.write_buffer;
wenzelm
parents: 27862
diff changeset
   378
      File.write_buffer (Path.append html_prefix (html_path a)) (Buffer.add HTML.end_document html);
11856
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
   379
24150
ed724867099a sort indexes according to symbolic update_time (multithreading-safe);
wenzelm
parents: 24102
diff changeset
   380
    val sorted_graph = sorted_index graph;
11856
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
   381
    val opt_graphs =
16263
0609fb8df4a7 removed copy, copy_all (superceded by File.copy, File.copy_dir);
wenzelm
parents: 15801
diff changeset
   382
      if doc_graph andalso (is_some doc_prefix1 orelse is_some doc_prefix2) then
28496
4cff10648928 renamed isatool to isabelle_tool in programming interfaces;
wenzelm
parents: 28375
diff changeset
   383
        SOME (isabelle_browser sorted_graph)
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15159
diff changeset
   384
      else NONE;
11856
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
   385
17210
e80fd664a119 added copy-dump option;
wenzelm
parents: 17177
diff changeset
   386
    fun prepare_sources cp path =
16263
0609fb8df4a7 removed copy, copy_all (superceded by File.copy, File.copy_dir);
wenzelm
parents: 15801
diff changeset
   387
     (File.mkdir path;
17210
e80fd664a119 added copy-dump option;
wenzelm
parents: 17177
diff changeset
   388
      if cp then File.copy_dir document_path path else ();
31819
2c0ab4485f48 tune File.isabelle_tool signature;
wenzelm
parents: 29606
diff changeset
   389
      File.isabelle_tool "latex"
2c0ab4485f48 tune File.isabelle_tool signature;
wenzelm
parents: 29606
diff changeset
   390
        ("-o sty " ^ File.shell_path (Path.append path (Path.basic "root.tex")));
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15159
diff changeset
   391
      (case opt_graphs of NONE => () | SOME (pdf, eps) =>
11856
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
   392
        (File.write (Path.append path graph_pdf_path) pdf;
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
   393
          File.write (Path.append path graph_eps_path) eps));
14922
88c1e108d0bf added Present.drafts;
wenzelm
parents: 14898
diff changeset
   394
      write_tex_index tex_index path;
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   395
      List.app (finish_tex path) thys);
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   396
  in
21962
279b129498b6 removed conditional combinator;
wenzelm
parents: 21858
diff changeset
   397
    if info then
11856
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
   398
     (File.mkdir (Path.append html_prefix session_path);
28027
051d5ccbafc5 renamed Buffer.write to File.write_buffer;
wenzelm
parents: 27862
diff changeset
   399
      File.write_buffer (Path.append html_prefix pre_index_path) (index_buffer html_index);
11856
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
   400
      File.write (Path.append html_prefix session_entries_path) "";
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
   401
      create_index html_prefix;
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
   402
      if length path > 1 then update_index parent_html_prefix name else ();
16263
0609fb8df4a7 removed copy, copy_all (superceded by File.copy, File.copy_dir);
wenzelm
parents: 15801
diff changeset
   403
      (case readme of NONE => () | SOME path => File.copy path html_prefix);
24150
ed724867099a sort indexes according to symbolic update_time (multithreading-safe);
wenzelm
parents: 24102
diff changeset
   404
      write_graph sorted_graph (Path.append html_prefix graph_path);
35588
f1429d5df3d2 finish browser_info: invoke isabelle browser -b to ensure that the jar really exists;
wenzelm
parents: 35010
diff changeset
   405
      File.isabelle_tool "browser" "-b";
21858
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 20664
diff changeset
   406
      File.copy (Path.explode "~~/lib/browser/GraphBrowser.jar") html_prefix;
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   407
      List.app (fn (a, txt) => File.write (Path.append html_prefix (Path.basic a)) txt)
14898
a25550451b51 Url.File;
wenzelm
parents: 14598
diff changeset
   408
        (HTML.applet_pages name (Url.File index_path, name));
21858
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 20664
diff changeset
   409
      File.copy (Path.explode "~~/lib/html/isabelle.css") html_prefix;
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   410
      List.app finish_html thys;
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   411
      List.app (uncurry File.write) files;
22580
d91b4dd651d6 cleaned-up Output functions;
wenzelm
parents: 22123
diff changeset
   412
      if verbose then Output.std_error ("Browser info at " ^ show_path html_prefix ^ "\n") else ())
21962
279b129498b6 removed conditional combinator;
wenzelm
parents: 21858
diff changeset
   413
    else ();
11856
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
   414
17210
e80fd664a119 added copy-dump option;
wenzelm
parents: 17177
diff changeset
   415
    (case doc_prefix2 of NONE => () | SOME (cp, path) =>
e80fd664a119 added copy-dump option;
wenzelm
parents: 17177
diff changeset
   416
     (prepare_sources cp path;
22580
d91b4dd651d6 cleaned-up Output functions;
wenzelm
parents: 22123
diff changeset
   417
      if verbose then Output.std_error ("Document sources at " ^ show_path path ^ "\n") else ()));
12895
d9dd528ecea6 clarified copy_all;
wenzelm
parents: 12849
diff changeset
   418
17082
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   419
    (case doc_prefix1 of NONE => () | SOME (path, result_path) =>
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   420
      documents |> List.app (fn (name, tags) =>
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   421
       let
17210
e80fd664a119 added copy-dump option;
wenzelm
parents: 17177
diff changeset
   422
         val _ = prepare_sources true path;
28496
4cff10648928 renamed isatool to isabelle_tool in programming interfaces;
wenzelm
parents: 28375
diff changeset
   423
         val doc_path = isabelle_document true doc_format name tags path result_path;
17082
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   424
       in
22580
d91b4dd651d6 cleaned-up Output functions;
wenzelm
parents: 22123
diff changeset
   425
         if verbose then Output.std_error ("Document at " ^ show_path doc_path ^ "\n") else ()
17082
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   426
       end));
11856
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
   427
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   428
    browser_info := empty_browser_info;
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15159
diff changeset
   429
    session_info := NONE
23944
2ea068548a83 marked some CRITICAL sections;
wenzelm
parents: 23899
diff changeset
   430
  end));
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   431
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   432
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   433
(* theory elements *)
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   434
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   435
fun init_theory name = with_session () (fn _ => init_theory_info name empty_theory_info);
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   436
27862
8f727f7c8c1d removed obsolete verbatim_source, results, chapter, section etc.;
wenzelm
parents: 27491
diff changeset
   437
fun theory_source name mk_text =
8f727f7c8c1d removed obsolete verbatim_source, results, chapter, section etc.;
wenzelm
parents: 27491
diff changeset
   438
  with_session () (fn _ => add_html_source name (HTML.theory_source (mk_text ())));
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   439
9136
8196955b02ec adapted to improved presentation;
wenzelm
parents: 9044
diff changeset
   440
fun theory_output name s =
9917
5af7632388a0 support \isabellecontext;
wenzelm
parents: 9795
diff changeset
   441
  with_session () (fn _ => add_tex_source name (Latex.isabelle_file name s));
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   442
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   443
23899
ab37b1f690c7 clarified init/begin_theory: no longer depend on thy_info.ML;
wenzelm
parents: 23884
diff changeset
   444
fun parent_link remote_path curr_session thy =
ab37b1f690c7 clarified init/begin_theory: no longer depend on thy_info.ML;
wenzelm
parents: 23884
diff changeset
   445
  let
ab37b1f690c7 clarified init/begin_theory: no longer depend on thy_info.ML;
wenzelm
parents: 23884
diff changeset
   446
    val {name = _, session, is_local} = get_info thy;
ab37b1f690c7 clarified init/begin_theory: no longer depend on thy_info.ML;
wenzelm
parents: 23884
diff changeset
   447
    val name = Context.theory_name thy;
ab37b1f690c7 clarified init/begin_theory: no longer depend on thy_info.ML;
wenzelm
parents: 23884
diff changeset
   448
    val link =
ab37b1f690c7 clarified init/begin_theory: no longer depend on thy_info.ML;
wenzelm
parents: 23884
diff changeset
   449
      if null session then NONE
ab37b1f690c7 clarified init/begin_theory: no longer depend on thy_info.ML;
wenzelm
parents: 23884
diff changeset
   450
      else SOME
ab37b1f690c7 clarified init/begin_theory: no longer depend on thy_info.ML;
wenzelm
parents: 23884
diff changeset
   451
       (if is_some remote_path andalso not is_local then
ab37b1f690c7 clarified init/begin_theory: no longer depend on thy_info.ML;
wenzelm
parents: 23884
diff changeset
   452
         Url.append (the remote_path) (Url.File (Path.append (Path.make session) (html_path name)))
ab37b1f690c7 clarified init/begin_theory: no longer depend on thy_info.ML;
wenzelm
parents: 23884
diff changeset
   453
        else Url.File (Path.append (mk_rel_path curr_session session) (html_path name)));
ab37b1f690c7 clarified init/begin_theory: no longer depend on thy_info.ML;
wenzelm
parents: 23884
diff changeset
   454
  in (link, name) end;
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   455
26323
73efc70edeef theory loader: discontinued *attached* ML scripts;
wenzelm
parents: 24829
diff changeset
   456
fun begin_theory update_time dir files thy =
9416
9144976964e7 removed all_sessions.graph;
wenzelm
parents: 9136
diff changeset
   457
    with_session thy (fn {name = sess_name, session, path, html_prefix, remote_path, ...} =>
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   458
  let
23899
ab37b1f690c7 clarified init/begin_theory: no longer depend on thy_info.ML;
wenzelm
parents: 23884
diff changeset
   459
    val name = Context.theory_name thy;
ab37b1f690c7 clarified init/begin_theory: no longer depend on thy_info.ML;
wenzelm
parents: 23884
diff changeset
   460
    val parents = Theory.parents_of thy;
ab37b1f690c7 clarified init/begin_theory: no longer depend on thy_info.ML;
wenzelm
parents: 23884
diff changeset
   461
    val parent_specs = map (parent_link remote_path path) parents;
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   462
37939
965537d86fcc discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents: 37216
diff changeset
   463
    val files_html = files |> map (fn (raw_path, loadit) =>
965537d86fcc discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents: 37216
diff changeset
   464
      let
38133
987680d2e77d simplified/clarified Thy_Load path: search for master only, lookup other files relative to that;
wenzelm
parents: 37940
diff changeset
   465
        val path = #1 (Thy_Load.check_file [dir] raw_path);
37939
965537d86fcc discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents: 37216
diff changeset
   466
        val base = Path.base path;
965537d86fcc discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents: 37216
diff changeset
   467
        val base_html = html_ext base;
965537d86fcc discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents: 37216
diff changeset
   468
        val _ = add_file (Path.append html_prefix base_html,
37940
4857eab31298 generic external source files -- nothing special about ML here;
wenzelm
parents: 37939
diff changeset
   469
          HTML.external_file (Url.File base) (File.read path));
37939
965537d86fcc discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents: 37216
diff changeset
   470
      in (Url.File base_html, Url.File raw_path, loadit) end);
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   471
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   472
    fun prep_html_source (tex_source, html_source, html) =
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   473
      let
14898
a25550451b51 Url.File;
wenzelm
parents: 14598
diff changeset
   474
        val txt = HTML.begin_theory (Url.File index_path, session)
27491
c8178a6a6480 begin_theory: files_html needs to be produced outside of prep_html_source to make ML files appear!
wenzelm
parents: 27329
diff changeset
   475
          name parent_specs files_html (Buffer.content html_source)
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   476
      in (tex_source, Buffer.empty, Buffer.add txt html) end;
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   477
9416
9144976964e7 removed all_sessions.graph;
wenzelm
parents: 9136
diff changeset
   478
    val entry =
9144976964e7 removed all_sessions.graph;
wenzelm
parents: 9136
diff changeset
   479
     {name = name, ID = ID_of path name, dir = sess_name, unfold = true,
21858
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 20664
diff changeset
   480
      path = Path.implode (html_path name),
23899
ab37b1f690c7 clarified init/begin_theory: no longer depend on thy_info.ML;
wenzelm
parents: 23884
diff changeset
   481
      parents = map ID_of_thy parents};
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   482
  in
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   483
    change_theory_info name prep_html_source;
24150
ed724867099a sort indexes according to symbolic update_time (multithreading-safe);
wenzelm
parents: 24102
diff changeset
   484
    add_graph_entry (update_time, entry);
ed724867099a sort indexes according to symbolic update_time (multithreading-safe);
wenzelm
parents: 24102
diff changeset
   485
    add_html_index (update_time, HTML.theory_entry (Url.File (html_path name), name));
ed724867099a sort indexes according to symbolic update_time (multithreading-safe);
wenzelm
parents: 24102
diff changeset
   486
    add_tex_index (update_time, Latex.theory_entry name);
27327
efd626efcb04 info: default name is "", not "Pure";
wenzelm
parents: 26957
diff changeset
   487
    put_info {name = sess_name, session = path, is_local = is_some remote_path} thy
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   488
  end);
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   489
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   490
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   491
14922
88c1e108d0bf added Present.drafts;
wenzelm
parents: 14898
diff changeset
   492
(** draft document output **)
88c1e108d0bf added Present.drafts;
wenzelm
parents: 14898
diff changeset
   493
88c1e108d0bf added Present.drafts;
wenzelm
parents: 14898
diff changeset
   494
fun drafts doc_format src_paths =
88c1e108d0bf added Present.drafts;
wenzelm
parents: 14898
diff changeset
   495
  let
24150
ed724867099a sort indexes according to symbolic update_time (multithreading-safe);
wenzelm
parents: 24102
diff changeset
   496
    fun prep_draft path i =
14935
c2441592be14 tuned Present.drafts;
wenzelm
parents: 14922
diff changeset
   497
      let
c2441592be14 tuned Present.drafts;
wenzelm
parents: 14922
diff changeset
   498
        val base = Path.base path;
14972
wenzelm
parents: 14967
diff changeset
   499
        val name =
24829
e1214fa781ca avoid gensym;
wenzelm
parents: 24561
diff changeset
   500
          (case Path.implode (#1 (Path.split_ext base)) of
e1214fa781ca avoid gensym;
wenzelm
parents: 24561
diff changeset
   501
            "" => "DUMMY" ^ serial_string ()
e1214fa781ca avoid gensym;
wenzelm
parents: 24561
diff changeset
   502
          | s => s);
14935
c2441592be14 tuned Present.drafts;
wenzelm
parents: 14922
diff changeset
   503
      in
c2441592be14 tuned Present.drafts;
wenzelm
parents: 14922
diff changeset
   504
        if File.exists path then
24150
ed724867099a sort indexes according to symbolic update_time (multithreading-safe);
wenzelm
parents: 24102
diff changeset
   505
          (((name, base, File.read path), (i, Latex.theory_entry name)), i + 1)
21858
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 20664
diff changeset
   506
        else error ("Bad file: " ^ quote (Path.implode path))
14935
c2441592be14 tuned Present.drafts;
wenzelm
parents: 14922
diff changeset
   507
      end;
24150
ed724867099a sort indexes according to symbolic update_time (multithreading-safe);
wenzelm
parents: 24102
diff changeset
   508
    val (srcs, tex_index) = split_list (fst (fold_map prep_draft src_paths 0));
14935
c2441592be14 tuned Present.drafts;
wenzelm
parents: 14922
diff changeset
   509
17082
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   510
    val doc_path = File.tmp_path document_path;
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   511
    val result_path = Path.append doc_path Path.parent;
14922
88c1e108d0bf added Present.drafts;
wenzelm
parents: 14898
diff changeset
   512
    val _ = File.mkdir doc_path;
88c1e108d0bf added Present.drafts;
wenzelm
parents: 14898
diff changeset
   513
    val root_path = Path.append doc_path (Path.basic "root.tex");
21858
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 20664
diff changeset
   514
    val _ = File.copy (Path.explode "~~/lib/texinputs/draft.tex") root_path;
31819
2c0ab4485f48 tune File.isabelle_tool signature;
wenzelm
parents: 29606
diff changeset
   515
    val _ = File.isabelle_tool "latex" ("-o sty " ^ File.shell_path root_path);
2c0ab4485f48 tune File.isabelle_tool signature;
wenzelm
parents: 29606
diff changeset
   516
    val _ = File.isabelle_tool "latex" ("-o syms " ^ File.shell_path root_path);
14922
88c1e108d0bf added Present.drafts;
wenzelm
parents: 14898
diff changeset
   517
88c1e108d0bf added Present.drafts;
wenzelm
parents: 14898
diff changeset
   518
    fun known name =
88c1e108d0bf added Present.drafts;
wenzelm
parents: 14898
diff changeset
   519
      let val ss = split_lines (File.read (Path.append doc_path (Path.basic name)))
20664
ffbc5a57191a member (op =);
wenzelm
parents: 20577
diff changeset
   520
      in member (op =) ss end;
14922
88c1e108d0bf added Present.drafts;
wenzelm
parents: 14898
diff changeset
   521
    val known_syms = known "syms.lst";
88c1e108d0bf added Present.drafts;
wenzelm
parents: 14898
diff changeset
   522
    val known_ctrls = known "ctrls.lst";
88c1e108d0bf added Present.drafts;
wenzelm
parents: 14898
diff changeset
   523
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   524
    val _ = srcs |> List.app (fn (name, base, txt) =>
14935
c2441592be14 tuned Present.drafts;
wenzelm
parents: 14922
diff changeset
   525
      Symbol.explode txt
21858
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 20664
diff changeset
   526
      |> Latex.symbol_source (known_syms, known_ctrls) (Path.implode base)
14935
c2441592be14 tuned Present.drafts;
wenzelm
parents: 14922
diff changeset
   527
      |> File.write (Path.append doc_path (tex_path name)));
14922
88c1e108d0bf added Present.drafts;
wenzelm
parents: 14898
diff changeset
   528
    val _ = write_tex_index tex_index doc_path;
28496
4cff10648928 renamed isatool to isabelle_tool in programming interfaces;
wenzelm
parents: 28375
diff changeset
   529
  in isabelle_document false doc_format documentN "" doc_path result_path end;
14922
88c1e108d0bf added Present.drafts;
wenzelm
parents: 14898
diff changeset
   530
88c1e108d0bf added Present.drafts;
wenzelm
parents: 14898
diff changeset
   531
7685
3edd32d588a6 improved theory_source presentation (hook);
wenzelm
parents: 6325
diff changeset
   532
end;
3edd32d588a6 improved theory_source presentation (hook);
wenzelm
parents: 6325
diff changeset
   533
32738
15bb09ca0378 explicit indication of Unsynchronized.ref;
wenzelm
parents: 31819
diff changeset
   534
structure Basic_Present: BASIC_PRESENT = Present;
15bb09ca0378 explicit indication of Unsynchronized.ref;
wenzelm
parents: 31819
diff changeset
   535
open Basic_Present;