src/Pure/Thy/present.ML
author wenzelm
Mon, 29 Aug 2011 21:55:49 +0200
changeset 44574 24444588fddd
parent 44389 a3b5fdfb04a3
child 44986 6f27ecf2a951
permissions -rw-r--r--
actual auto loading of required files; eliminated File_Store in favour of Thy_Load; tuned;
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
42008
7423e833a880 Present.init/finish/no_document are not thread-safe -- eliminated futile CRITICAL sections;
wenzelm
parents: 42007
diff changeset
     9
  val no_document: ('a -> 'b) -> 'a -> 'b  (*not thread-safe!*)
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 ->
42008
7423e833a880 Present.init/finish/no_document are not thread-safe -- eliminated futile CRITICAL sections;
wenzelm
parents: 42007
diff changeset
    21
    string -> (bool * Path.T) option -> Url.T option * bool -> bool ->
7423e833a880 Present.init/finish/no_document are not thread-safe -- eliminated futile CRITICAL sections;
wenzelm
parents: 42007
diff changeset
    22
    theory list -> unit  (*not thread-safe!*)
7423e833a880 Present.init/finish/no_document are not thread-safe -- eliminated futile CRITICAL sections;
wenzelm
parents: 42007
diff changeset
    23
  val finish: unit -> unit  (*not thread-safe!*)
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
    24
  val init_theory: string -> unit
27862
8f727f7c8c1d removed obsolete verbatim_source, results, chapter, section etc.;
wenzelm
parents: 27491
diff changeset
    25
  val theory_source: string -> (unit -> HTML.text) -> unit
9136
8196955b02ec adapted to improved presentation;
wenzelm
parents: 9044
diff changeset
    26
  val theory_output: string -> string -> unit
24150
ed724867099a sort indexes according to symbolic update_time (multithreading-safe);
wenzelm
parents: 24102
diff changeset
    27
  val begin_theory: int -> Path.T -> (Path.T * bool) list -> theory -> theory
14922
88c1e108d0bf added Present.drafts;
wenzelm
parents: 14898
diff changeset
    28
  val drafts: string -> Path.T list -> Path.T
6203
328b4377755c Theory presentation (fake implementation);
wenzelm
parents:
diff changeset
    29
end;
328b4377755c Theory presentation (fake implementation);
wenzelm
parents:
diff changeset
    30
7685
3edd32d588a6 improved theory_source presentation (hook);
wenzelm
parents: 6325
diff changeset
    31
structure Present: PRESENT =
3edd32d588a6 improved theory_source presentation (hook);
wenzelm
parents: 6325
diff changeset
    32
struct
3edd32d588a6 improved theory_source presentation (hook);
wenzelm
parents: 6325
diff changeset
    33
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
    34
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
    35
(** paths **)
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
    36
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
    37
val output_path = Path.variable "ISABELLE_BROWSER_INFO";
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
    38
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
    39
val tex_ext = Path.ext "tex";
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
    40
val tex_path = tex_ext o Path.basic;
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
    41
val html_ext = Path.ext "html";
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
    42
val html_path = html_ext o Path.basic;
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
    43
val index_path = Path.basic "index.html";
11856
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
    44
val readme_html_path = Path.basic "README.html";
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
    45
val readme_path = Path.basic "README";
17082
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
    46
val documentN = "document";
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
    47
val document_path = Path.basic documentN;
8196
ecb9decd38ac additional tex dump;
wenzelm
parents: 8192
diff changeset
    48
val doc_indexN = "session";
11856
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
    49
val graph_path = Path.basic "session.graph";
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
    50
val graph_pdf_path = Path.basic "session_graph.pdf";
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
    51
val graph_eps_path = Path.basic "session_graph.eps";
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
    52
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
    53
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
    54
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
    55
val pre_index_path = Path.explode ".session/pre-index";
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
    56
9044
28ee037278a6 Reorganized graph stuff.
berghofe
parents: 8808
diff changeset
    57
fun mk_rel_path [] ys = Path.make ys
28ee037278a6 Reorganized graph stuff.
berghofe
parents: 8808
diff changeset
    58
  | mk_rel_path xs [] = Path.appends (replicate (length xs) Path.parent)
9416
9144976964e7 removed all_sessions.graph;
wenzelm
parents: 9136
diff changeset
    59
  | 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
    60
      Path.appends (replicate (length ps) Path.parent @ [Path.make qs]);
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
    61
21858
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 20664
diff changeset
    62
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
    63
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
    64
14922
88c1e108d0bf added Present.drafts;
wenzelm
parents: 14898
diff changeset
    65
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
    66
(** additional theory data **)
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
    67
42008
7423e833a880 Present.init/finish/no_document are not thread-safe -- eliminated futile CRITICAL sections;
wenzelm
parents: 42007
diff changeset
    68
structure Browser_Info = Theory_Data
22846
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22580
diff changeset
    69
(
9416
9144976964e7 removed all_sessions.graph;
wenzelm
parents: 9136
diff changeset
    70
  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
    71
  val empty = {name = "", session = [], is_local = false}: T;
16503
24491bde68df clarify empty vs. pure browser info;
wenzelm
parents: 16426
diff changeset
    72
  fun extend _ = empty;
33522
737589bb9bb8 adapted Theory_Data;
wenzelm
parents: 32738
diff changeset
    73
  fun merge _ = empty;
22846
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22580
diff changeset
    74
);
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
    75
42008
7423e833a880 Present.init/finish/no_document are not thread-safe -- eliminated futile CRITICAL sections;
wenzelm
parents: 42007
diff changeset
    76
val put_info = Browser_Info.put;
7423e833a880 Present.init/finish/no_document are not thread-safe -- eliminated futile CRITICAL sections;
wenzelm
parents: 42007
diff changeset
    77
val get_info = Browser_Info.get;
24561
7b4aa14d2491 tuned signature;
wenzelm
parents: 24150
diff changeset
    78
val session_name = #name o get_info;
7b4aa14d2491 tuned signature;
wenzelm
parents: 24150
diff changeset
    79
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
    80
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
    81
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
    82
(** graphs **)
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
    83
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
    84
type graph_node =
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
    85
  {name: string, ID: string, dir: string, unfold: bool,
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
    86
   path: string, parents: string list};
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
    87
9416
9144976964e7 removed all_sessions.graph;
wenzelm
parents: 9136
diff changeset
    88
fun write_graph gr path =
9144976964e7 removed all_sessions.graph;
wenzelm
parents: 9136
diff changeset
    89
  File.write path (cat_lines (map (fn {name, ID, dir, unfold, path, parents} =>
9144976964e7 removed all_sessions.graph;
wenzelm
parents: 9136
diff changeset
    90
    "\"" ^ name ^ "\" \"" ^ ID ^ "\" \"" ^ dir ^ (if unfold then "\" + \"" else "\" \"") ^
28840
wenzelm
parents: 28500
diff changeset
    91
    path ^ "\" > " ^ space_implode " " (map quote parents) ^ " ;") gr));
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
    92
20577
a96883a6d709 added display_graph (from thm_deps.ML);
wenzelm
parents: 19305
diff changeset
    93
fun display_graph gr =
a96883a6d709 added display_graph (from thm_deps.ML);
wenzelm
parents: 19305
diff changeset
    94
  let
42127
8223e7f4b0da Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
wenzelm
parents: 42126
diff changeset
    95
    val path = Isabelle_System.create_tmp_path "graph" "";
8223e7f4b0da Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
wenzelm
parents: 42126
diff changeset
    96
    val _ = write_graph gr path;
24561
7b4aa14d2491 tuned signature;
wenzelm
parents: 24150
diff changeset
    97
    val _ = writeln "Displaying graph ...";
40743
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents: 39733
diff changeset
    98
    val _ = Isabelle_System.isabelle_tool "browser" ("-c " ^ File.shell_path path ^ " &");
20577
a96883a6d709 added display_graph (from thm_deps.ML);
wenzelm
parents: 19305
diff changeset
    99
  in () end;
a96883a6d709 added display_graph (from thm_deps.ML);
wenzelm
parents: 19305
diff changeset
   100
a96883a6d709 added display_graph (from thm_deps.ML);
wenzelm
parents: 19305
diff changeset
   101
9416
9144976964e7 removed all_sessions.graph;
wenzelm
parents: 9136
diff changeset
   102
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
   103
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
   104
23899
ab37b1f690c7 clarified init/begin_theory: no longer depend on thy_info.ML;
wenzelm
parents: 23884
diff changeset
   105
ab37b1f690c7 clarified init/begin_theory: no longer depend on thy_info.ML;
wenzelm
parents: 23884
diff changeset
   106
(*retrieve graph data from initial collection of theories*)
24150
ed724867099a sort indexes according to symbolic update_time (multithreading-safe);
wenzelm
parents: 24102
diff changeset
   107
fun init_graph remote_path curr_sess = rev o map (fn thy =>
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   108
  let
23899
ab37b1f690c7 clarified init/begin_theory: no longer depend on thy_info.ML;
wenzelm
parents: 23884
diff changeset
   109
    val name = Context.theory_name thy;
ab37b1f690c7 clarified init/begin_theory: no longer depend on thy_info.ML;
wenzelm
parents: 23884
diff changeset
   110
    val {name = sess_name, session, is_local} = get_info thy;
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;
42008
7423e833a880 Present.init/finish/no_document are not thread-safe -- eliminated futile CRITICAL sections;
wenzelm
parents: 42007
diff changeset
   168
fun no_document f x = Unsynchronized.setmp suppress_tex_source true f x;
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 =
42010
04f8c4851219 eliminated dead code;
wenzelm
parents: 42009
diff changeset
   175
  change_browser_info (fn (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
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   207
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   208
(** global session state **)
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   209
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   210
(* session_info *)
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   211
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   212
type session_info =
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   213
  {name: string, parent: string, session: string, path: string list, html_prefix: Path.T,
17082
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   214
    info: bool, doc_format: string, doc_graph: bool, documents: (string * string) list,
42007
2142883ec29f eliminated redundant doc_prefix1;
wenzelm
parents: 42006
diff changeset
   215
    dump_prefix: (bool * Path.T) option, remote_path: Url.T option, verbose: bool,
2142883ec29f eliminated redundant doc_prefix1;
wenzelm
parents: 42006
diff changeset
   216
    readme: Path.T option};
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   217
9416
9144976964e7 removed all_sessions.graph;
wenzelm
parents: 9136
diff changeset
   218
fun make_session_info
17082
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   219
  (name, parent, session, path, html_prefix, info, doc_format, doc_graph, documents,
42007
2142883ec29f eliminated redundant doc_prefix1;
wenzelm
parents: 42006
diff changeset
   220
    dump_prefix, remote_path, verbose, readme) =
7802
fba7a36e8556 isatool_document;
wenzelm
parents: 7789
diff changeset
   221
  {name = name, parent = parent, session = session, path = path, html_prefix = html_prefix,
17082
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   222
    info = info, doc_format = doc_format, doc_graph = doc_graph, documents = documents,
42007
2142883ec29f eliminated redundant doc_prefix1;
wenzelm
parents: 42006
diff changeset
   223
    dump_prefix = dump_prefix, remote_path = remote_path, verbose = verbose,
2142883ec29f eliminated redundant doc_prefix1;
wenzelm
parents: 42006
diff changeset
   224
    readme = readme}: session_info;
7685
3edd32d588a6 improved theory_source presentation (hook);
wenzelm
parents: 6325
diff changeset
   225
3edd32d588a6 improved theory_source presentation (hook);
wenzelm
parents: 6325
diff changeset
   226
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   227
(* state *)
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   228
32738
15bb09ca0378 explicit indication of Unsynchronized.ref;
wenzelm
parents: 31819
diff changeset
   229
val session_info = Unsynchronized.ref (NONE: session_info option);
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   230
42126
wenzelm
parents: 42010
diff changeset
   231
fun session_default x f = (case ! session_info of NONE => x | SOME info => f info);
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   232
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   233
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   234
14922
88c1e108d0bf added Present.drafts;
wenzelm
parents: 14898
diff changeset
   235
(** document preparation **)
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   236
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   237
(* maintain index *)
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   238
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   239
val session_entries =
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   240
  HTML.session_entries o
14898
a25550451b51 Url.File;
wenzelm
parents: 14598
diff changeset
   241
    map (fn name => (Url.File (Path.append (Path.basic name) index_path), name));
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   242
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   243
fun get_entries dir =
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   244
  split_lines (File.read (Path.append dir session_entries_path));
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   245
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   246
fun put_entries entries dir =
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   247
  File.write (Path.append dir session_entries_path) (cat_lines entries);
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   248
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   249
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   250
fun create_index dir =
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   251
  File.read (Path.append dir pre_index_path) ^
27862
8f727f7c8c1d removed obsolete verbatim_source, results, chapter, section etc.;
wenzelm
parents: 27491
diff changeset
   252
    session_entries (get_entries dir) ^ HTML.end_document
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   253
  |> File.write (Path.append dir index_path);
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   254
42008
7423e833a880 Present.init/finish/no_document are not thread-safe -- eliminated futile CRITICAL sections;
wenzelm
parents: 42007
diff changeset
   255
fun update_index dir name =
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   256
  (case try get_entries dir of
41944
b97091ae583a Path.print is the official way to show file-system paths to users -- note that Path.implode often indicates violation of the abstract datatype;
wenzelm
parents: 41886
diff changeset
   257
    NONE => warning ("Browser info: cannot access session index of " ^ Path.print dir)
42008
7423e833a880 Present.init/finish/no_document are not thread-safe -- eliminated futile CRITICAL sections;
wenzelm
parents: 42007
diff changeset
   258
  | SOME es => (put_entries ((remove (op =) name es) @ [name]) dir; create_index dir));
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   259
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   260
42004
e06351ffb475 tuned terminology for document variants;
wenzelm
parents: 42003
diff changeset
   261
(* document variants *)
17082
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   262
42004
e06351ffb475 tuned terminology for document variants;
wenzelm
parents: 42003
diff changeset
   263
fun read_variant str =
17082
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   264
  (case space_explode "=" str of
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   265
    [name] => (name, "")
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   266
  | [name, tags] => (name, tags)
42004
e06351ffb475 tuned terminology for document variants;
wenzelm
parents: 42003
diff changeset
   267
  | _ => error ("Malformed document variant specification: " ^ quote str));
17082
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   268
42004
e06351ffb475 tuned terminology for document variants;
wenzelm
parents: 42003
diff changeset
   269
fun read_variants strs =
e06351ffb475 tuned terminology for document variants;
wenzelm
parents: 42003
diff changeset
   270
  rev (distinct (eq_fst (op =)) (rev ((documentN, "") :: map read_variant strs)))
28375
c879d88d038a eliminated polymorphic equality;
wenzelm
parents: 28027
diff changeset
   271
  |> filter_out (fn (_, s) => s = "-");
17082
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   272
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   273
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   274
(* init session *)
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   275
12895
d9dd528ecea6 clarified copy_all;
wenzelm
parents: 12849
diff changeset
   276
fun name_of_session elems = space_implode "/" ("Isabelle" :: elems);
d9dd528ecea6 clarified copy_all;
wenzelm
parents: 12849
diff changeset
   277
42006
7eecd020e367 renamed doc_prefix2 to dump_prefix;
wenzelm
parents: 42005
diff changeset
   278
fun init build info doc doc_graph doc_variants path name dump_prefix
42008
7423e833a880 Present.init/finish/no_document are not thread-safe -- eliminated futile CRITICAL sections;
wenzelm
parents: 42007
diff changeset
   279
    (remote_path, first_time) verbose thys =
42006
7eecd020e367 renamed doc_prefix2 to dump_prefix;
wenzelm
parents: 42005
diff changeset
   280
  if not build andalso not info andalso doc = "" andalso is_none dump_prefix then
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15159
diff changeset
   281
    (browser_info := empty_browser_info; session_info := NONE)
11856
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
   282
  else
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
   283
    let
33957
e9afca2118d4 normalized uncurry take/drop
haftmann
parents: 33955
diff changeset
   284
      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
   285
      val session_name = name_of_session path;
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
   286
      val sess_prefix = Path.make path;
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
   287
      val html_prefix = Path.append (Path.expand output_path) sess_prefix;
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   288
42007
2142883ec29f eliminated redundant doc_prefix1;
wenzelm
parents: 42006
diff changeset
   289
      val documents =
2142883ec29f eliminated redundant doc_prefix1;
wenzelm
parents: 42006
diff changeset
   290
        if doc = "" then []
42005
wenzelm
parents: 42004
diff changeset
   291
        else if not (can File.check_dir document_path) then
44389
a3b5fdfb04a3 tuned signature -- contrast physical output primitives versus Output.raw_message;
wenzelm
parents: 43850
diff changeset
   292
          (if verbose then Output.physical_stderr "Warning: missing document directory\n"
a3b5fdfb04a3 tuned signature -- contrast physical output primitives versus Output.raw_message;
wenzelm
parents: 43850
diff changeset
   293
           else (); [])
42007
2142883ec29f eliminated redundant doc_prefix1;
wenzelm
parents: 42006
diff changeset
   294
        else read_variants doc_variants;
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   295
11856
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
   296
      val parent_index_path = Path.append Path.parent index_path;
42007
2142883ec29f eliminated redundant doc_prefix1;
wenzelm
parents: 42006
diff changeset
   297
      val index_up_lnk =
2142883ec29f eliminated redundant doc_prefix1;
wenzelm
parents: 42006
diff changeset
   298
        if first_time then
16263
0609fb8df4a7 removed copy, copy_all (superceded by File.copy, File.copy_dir);
wenzelm
parents: 15801
diff changeset
   299
          Url.append (the remote_path) (Url.File (Path.append sess_prefix parent_index_path))
14898
a25550451b51 Url.File;
wenzelm
parents: 14598
diff changeset
   300
        else Url.File parent_index_path;
11856
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
   301
      val readme =
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15159
diff changeset
   302
        if File.exists readme_html_path then SOME readme_html_path
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15159
diff changeset
   303
        else if File.exists readme_path then SOME readme_path
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15159
diff changeset
   304
        else NONE;
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   305
17082
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   306
      val docs =
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   307
        (case readme of NONE => [] | SOME p => [(Url.File p, "README")]) @
42007
2142883ec29f eliminated redundant doc_prefix1;
wenzelm
parents: 42006
diff changeset
   308
          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
   309
      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
   310
        (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
   311
    in
42007
2142883ec29f eliminated redundant doc_prefix1;
wenzelm
parents: 42006
diff changeset
   312
      session_info :=
2142883ec29f eliminated redundant doc_prefix1;
wenzelm
parents: 42006
diff changeset
   313
        SOME (make_session_info (name, parent_name, session_name, path, html_prefix,
2142883ec29f eliminated redundant doc_prefix1;
wenzelm
parents: 42006
diff changeset
   314
          info, doc, doc_graph, documents, dump_prefix, remote_path, verbose, readme));
23899
ab37b1f690c7 clarified init/begin_theory: no longer depend on thy_info.ML;
wenzelm
parents: 23884
diff changeset
   315
      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
   316
      add_html_index (0, index_text)
42008
7423e833a880 Present.init/finish/no_document are not thread-safe -- eliminated futile CRITICAL sections;
wenzelm
parents: 42007
diff changeset
   317
    end;
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   318
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   319
28496
4cff10648928 renamed isatool to isabelle_tool in programming interfaces;
wenzelm
parents: 28375
diff changeset
   320
(* isabelle tool wrappers *)
17082
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   321
28496
4cff10648928 renamed isatool to isabelle_tool in programming interfaces;
wenzelm
parents: 28375
diff changeset
   322
fun isabelle_document verbose format name tags path result_path =
17082
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   323
  let
28500
4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL;
wenzelm
parents: 28496
diff changeset
   324
    val s = "\"$ISABELLE_TOOL\" document -c -o '" ^ format ^ "' \
33682
0c5d1485dea7 isabelle_document: more explicit error output, notably for drafts;
wenzelm
parents: 33522
diff changeset
   325
      \-n '" ^ name ^ "' -t '" ^ tags ^ "' " ^ File.shell_path path ^ " 2>&1";
17082
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   326
    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
   327
    val _ = if verbose then writeln s else ();
43850
7f2cbc713344 moved bash operations to Isabelle_System (cf. Scala version);
wenzelm
parents: 43712
diff changeset
   328
    val (out, rc) = Isabelle_System.bash_output s;
33682
0c5d1485dea7 isabelle_document: more explicit error output, notably for drafts;
wenzelm
parents: 33522
diff changeset
   329
    val _ =
0c5d1485dea7 isabelle_document: more explicit error output, notably for drafts;
wenzelm
parents: 33522
diff changeset
   330
      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
   331
        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
   332
      else if verbose then writeln out
0c5d1485dea7 isabelle_document: more explicit error output, notably for drafts;
wenzelm
parents: 33522
diff changeset
   333
      else ();
0c5d1485dea7 isabelle_document: more explicit error output, notably for drafts;
wenzelm
parents: 33522
diff changeset
   334
  in doc_path end;
17082
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   335
42127
8223e7f4b0da Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
wenzelm
parents: 42126
diff changeset
   336
fun isabelle_browser graph = Isabelle_System.with_tmp_dir "browser" (fn dir =>
17082
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   337
  let
42127
8223e7f4b0da Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
wenzelm
parents: 42126
diff changeset
   338
    val pdf_path = Path.append dir graph_pdf_path;
8223e7f4b0da Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
wenzelm
parents: 42126
diff changeset
   339
    val eps_path = Path.append dir graph_eps_path;
8223e7f4b0da Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
wenzelm
parents: 42126
diff changeset
   340
    val graph_path = Path.append dir graph_path;
8223e7f4b0da Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
wenzelm
parents: 42126
diff changeset
   341
    val _ = write_graph graph graph_path;
8223e7f4b0da Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
wenzelm
parents: 42126
diff changeset
   342
    val args = "-o " ^ File.shell_path pdf_path ^ " " ^ File.shell_path graph_path;
17082
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   343
  in
42127
8223e7f4b0da Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
wenzelm
parents: 42126
diff changeset
   344
    if Isabelle_System.isabelle_tool "browser" args = 0 andalso
8223e7f4b0da Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
wenzelm
parents: 42126
diff changeset
   345
      File.exists pdf_path andalso File.exists eps_path
8223e7f4b0da Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
wenzelm
parents: 42126
diff changeset
   346
    then (File.read pdf_path, File.read eps_path)
8223e7f4b0da Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
wenzelm
parents: 42126
diff changeset
   347
    else error "Failed to prepare dependency graph"
8223e7f4b0da Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
wenzelm
parents: 42126
diff changeset
   348
  end);
17082
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   349
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   350
11856
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
   351
(* finish session -- output all generated text *)
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
   352
24150
ed724867099a sort indexes according to symbolic update_time (multithreading-safe);
wenzelm
parents: 24102
diff changeset
   353
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
   354
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
   355
14922
88c1e108d0bf added Present.drafts;
wenzelm
parents: 14898
diff changeset
   356
fun write_tex src name path =
28027
051d5ccbafc5 renamed Buffer.write to File.write_buffer;
wenzelm
parents: 27862
diff changeset
   357
  File.write_buffer (Path.append path (tex_path name)) src;
14922
88c1e108d0bf added Present.drafts;
wenzelm
parents: 14898
diff changeset
   358
88c1e108d0bf added Present.drafts;
wenzelm
parents: 14898
diff changeset
   359
fun write_tex_index tex_index path =
24150
ed724867099a sort indexes according to symbolic update_time (multithreading-safe);
wenzelm
parents: 24102
diff changeset
   360
  write_tex (index_buffer tex_index |> Buffer.add Latex.tex_trailer) doc_indexN path;
14922
88c1e108d0bf added Present.drafts;
wenzelm
parents: 14898
diff changeset
   361
7685
3edd32d588a6 improved theory_source presentation (hook);
wenzelm
parents: 6325
diff changeset
   362
42008
7423e833a880 Present.init/finish/no_document are not thread-safe -- eliminated futile CRITICAL sections;
wenzelm
parents: 42007
diff changeset
   363
fun finish () =
42126
wenzelm
parents: 42010
diff changeset
   364
  session_default () (fn {name, info, html_prefix, doc_format,
42008
7423e833a880 Present.init/finish/no_document are not thread-safe -- eliminated futile CRITICAL sections;
wenzelm
parents: 42007
diff changeset
   365
    doc_graph, documents, dump_prefix, path, verbose, readme, ...} =>
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   366
  let
11856
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
   367
    val {theories, files, tex_index, html_index, graph} = ! browser_info;
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
   368
    val thys = Symtab.dest theories;
9416
9144976964e7 removed all_sessions.graph;
wenzelm
parents: 9136
diff changeset
   369
    val parent_html_prefix = Path.append html_prefix Path.parent;
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   370
11856
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
   371
    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
   372
    fun finish_html (a, {html, ...}: theory_info) =
28027
051d5ccbafc5 renamed Buffer.write to File.write_buffer;
wenzelm
parents: 27862
diff changeset
   373
      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
   374
24150
ed724867099a sort indexes according to symbolic update_time (multithreading-safe);
wenzelm
parents: 24102
diff changeset
   375
    val sorted_graph = sorted_index graph;
11856
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
   376
    val opt_graphs =
42007
2142883ec29f eliminated redundant doc_prefix1;
wenzelm
parents: 42006
diff changeset
   377
      if doc_graph andalso (not (null documents) orelse is_some dump_prefix) then
28496
4cff10648928 renamed isatool to isabelle_tool in programming interfaces;
wenzelm
parents: 28375
diff changeset
   378
        SOME (isabelle_browser sorted_graph)
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15159
diff changeset
   379
      else NONE;
11856
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
   380
17210
e80fd664a119 added copy-dump option;
wenzelm
parents: 17177
diff changeset
   381
    fun prepare_sources cp path =
40743
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents: 39733
diff changeset
   382
     (Isabelle_System.mkdirs path;
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents: 39733
diff changeset
   383
      if cp then Isabelle_System.copy_dir document_path path else ();
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents: 39733
diff changeset
   384
      Isabelle_System.isabelle_tool "latex"
31819
2c0ab4485f48 tune File.isabelle_tool signature;
wenzelm
parents: 29606
diff changeset
   385
        ("-o sty " ^ File.shell_path (Path.append path (Path.basic "root.tex")));
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15159
diff changeset
   386
      (case opt_graphs of NONE => () | SOME (pdf, eps) =>
11856
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
   387
        (File.write (Path.append path graph_pdf_path) pdf;
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
   388
          File.write (Path.append path graph_eps_path) eps));
14922
88c1e108d0bf added Present.drafts;
wenzelm
parents: 14898
diff changeset
   389
      write_tex_index tex_index path;
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   390
      List.app (finish_tex path) thys);
42007
2142883ec29f eliminated redundant doc_prefix1;
wenzelm
parents: 42006
diff changeset
   391
    val _ =
2142883ec29f eliminated redundant doc_prefix1;
wenzelm
parents: 42006
diff changeset
   392
      if info then
2142883ec29f eliminated redundant doc_prefix1;
wenzelm
parents: 42006
diff changeset
   393
       (Isabelle_System.mkdirs (Path.append html_prefix session_path);
2142883ec29f eliminated redundant doc_prefix1;
wenzelm
parents: 42006
diff changeset
   394
        File.write_buffer (Path.append html_prefix pre_index_path) (index_buffer html_index);
2142883ec29f eliminated redundant doc_prefix1;
wenzelm
parents: 42006
diff changeset
   395
        File.write (Path.append html_prefix session_entries_path) "";
2142883ec29f eliminated redundant doc_prefix1;
wenzelm
parents: 42006
diff changeset
   396
        create_index html_prefix;
2142883ec29f eliminated redundant doc_prefix1;
wenzelm
parents: 42006
diff changeset
   397
        if length path > 1 then update_index parent_html_prefix name else ();
2142883ec29f eliminated redundant doc_prefix1;
wenzelm
parents: 42006
diff changeset
   398
        (case readme of NONE => () | SOME path => File.copy path html_prefix);
2142883ec29f eliminated redundant doc_prefix1;
wenzelm
parents: 42006
diff changeset
   399
        write_graph sorted_graph (Path.append html_prefix graph_path);
2142883ec29f eliminated redundant doc_prefix1;
wenzelm
parents: 42006
diff changeset
   400
        Isabelle_System.isabelle_tool "browser" "-b";
2142883ec29f eliminated redundant doc_prefix1;
wenzelm
parents: 42006
diff changeset
   401
        File.copy (Path.explode "~~/lib/browser/GraphBrowser.jar") html_prefix;
2142883ec29f eliminated redundant doc_prefix1;
wenzelm
parents: 42006
diff changeset
   402
        List.app (fn (a, txt) => File.write (Path.append html_prefix (Path.basic a)) txt)
2142883ec29f eliminated redundant doc_prefix1;
wenzelm
parents: 42006
diff changeset
   403
          (HTML.applet_pages name (Url.File index_path, name));
43437
55866987a7d9 proper place for config files;
wenzelm
parents: 42127
diff changeset
   404
        File.copy (Path.explode "~~/etc/isabelle.css") html_prefix;
42007
2142883ec29f eliminated redundant doc_prefix1;
wenzelm
parents: 42006
diff changeset
   405
        List.app finish_html thys;
2142883ec29f eliminated redundant doc_prefix1;
wenzelm
parents: 42006
diff changeset
   406
        List.app (uncurry File.write) files;
44389
a3b5fdfb04a3 tuned signature -- contrast physical output primitives versus Output.raw_message;
wenzelm
parents: 43850
diff changeset
   407
        if verbose then Output.physical_stderr ("Browser info at " ^ show_path html_prefix ^ "\n")
42007
2142883ec29f eliminated redundant doc_prefix1;
wenzelm
parents: 42006
diff changeset
   408
        else ())
2142883ec29f eliminated redundant doc_prefix1;
wenzelm
parents: 42006
diff changeset
   409
      else ();
2142883ec29f eliminated redundant doc_prefix1;
wenzelm
parents: 42006
diff changeset
   410
2142883ec29f eliminated redundant doc_prefix1;
wenzelm
parents: 42006
diff changeset
   411
    val _ =
2142883ec29f eliminated redundant doc_prefix1;
wenzelm
parents: 42006
diff changeset
   412
      (case dump_prefix of NONE => () | SOME (cp, path) =>
2142883ec29f eliminated redundant doc_prefix1;
wenzelm
parents: 42006
diff changeset
   413
       (prepare_sources cp path;
44389
a3b5fdfb04a3 tuned signature -- contrast physical output primitives versus Output.raw_message;
wenzelm
parents: 43850
diff changeset
   414
        if verbose then Output.physical_stderr ("Document sources at " ^ show_path path ^ "\n")
42007
2142883ec29f eliminated redundant doc_prefix1;
wenzelm
parents: 42006
diff changeset
   415
        else ()));
2142883ec29f eliminated redundant doc_prefix1;
wenzelm
parents: 42006
diff changeset
   416
2142883ec29f eliminated redundant doc_prefix1;
wenzelm
parents: 42006
diff changeset
   417
    val doc_paths =
42009
b008525c4399 parallel preparation of document variants, within separate directories;
wenzelm
parents: 42008
diff changeset
   418
      documents |> Par_List.map (fn (name, tags) =>
42007
2142883ec29f eliminated redundant doc_prefix1;
wenzelm
parents: 42006
diff changeset
   419
        let
42009
b008525c4399 parallel preparation of document variants, within separate directories;
wenzelm
parents: 42008
diff changeset
   420
          val path = Path.append html_prefix (Path.basic name);
42007
2142883ec29f eliminated redundant doc_prefix1;
wenzelm
parents: 42006
diff changeset
   421
          val _ = prepare_sources true path;
2142883ec29f eliminated redundant doc_prefix1;
wenzelm
parents: 42006
diff changeset
   422
        in isabelle_document true doc_format name tags path html_prefix end);
2142883ec29f eliminated redundant doc_prefix1;
wenzelm
parents: 42006
diff changeset
   423
    val _ =
2142883ec29f eliminated redundant doc_prefix1;
wenzelm
parents: 42006
diff changeset
   424
      if verbose then
44389
a3b5fdfb04a3 tuned signature -- contrast physical output primitives versus Output.raw_message;
wenzelm
parents: 43850
diff changeset
   425
        doc_paths
a3b5fdfb04a3 tuned signature -- contrast physical output primitives versus Output.raw_message;
wenzelm
parents: 43850
diff changeset
   426
        |> List.app (fn doc => Output.physical_stderr ("Document at " ^ show_path doc ^ "\n"))
42007
2142883ec29f eliminated redundant doc_prefix1;
wenzelm
parents: 42006
diff changeset
   427
      else ();
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   428
  in
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   429
    browser_info := empty_browser_info;
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15159
diff changeset
   430
    session_info := NONE
42008
7423e833a880 Present.init/finish/no_document are not thread-safe -- eliminated futile CRITICAL sections;
wenzelm
parents: 42007
diff changeset
   431
  end);
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   432
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   433
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   434
(* theory elements *)
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   435
42126
wenzelm
parents: 42010
diff changeset
   436
fun init_theory name = session_default () (fn _ => init_theory_info name empty_theory_info);
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   437
27862
8f727f7c8c1d removed obsolete verbatim_source, results, chapter, section etc.;
wenzelm
parents: 27491
diff changeset
   438
fun theory_source name mk_text =
42126
wenzelm
parents: 42010
diff changeset
   439
  session_default () (fn _ => add_html_source name (HTML.theory_source (mk_text ())));
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   440
9136
8196955b02ec adapted to improved presentation;
wenzelm
parents: 9044
diff changeset
   441
fun theory_output name s =
42126
wenzelm
parents: 42010
diff changeset
   442
  session_default () (fn _ => add_tex_source name (Latex.isabelle_file name s));
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   443
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   444
23899
ab37b1f690c7 clarified init/begin_theory: no longer depend on thy_info.ML;
wenzelm
parents: 23884
diff changeset
   445
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
   446
  let
ab37b1f690c7 clarified init/begin_theory: no longer depend on thy_info.ML;
wenzelm
parents: 23884
diff changeset
   447
    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
   448
    val name = Context.theory_name thy;
ab37b1f690c7 clarified init/begin_theory: no longer depend on thy_info.ML;
wenzelm
parents: 23884
diff changeset
   449
    val link =
ab37b1f690c7 clarified init/begin_theory: no longer depend on thy_info.ML;
wenzelm
parents: 23884
diff changeset
   450
      if null session then NONE
ab37b1f690c7 clarified init/begin_theory: no longer depend on thy_info.ML;
wenzelm
parents: 23884
diff changeset
   451
      else SOME
ab37b1f690c7 clarified init/begin_theory: no longer depend on thy_info.ML;
wenzelm
parents: 23884
diff changeset
   452
       (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
   453
         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
   454
        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
   455
  in (link, name) end;
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   456
26323
73efc70edeef theory loader: discontinued *attached* ML scripts;
wenzelm
parents: 24829
diff changeset
   457
fun begin_theory update_time dir files thy =
42126
wenzelm
parents: 42010
diff changeset
   458
    session_default thy (fn {name = sess_name, session, path, html_prefix, remote_path, ...} =>
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   459
  let
23899
ab37b1f690c7 clarified init/begin_theory: no longer depend on thy_info.ML;
wenzelm
parents: 23884
diff changeset
   460
    val name = Context.theory_name thy;
ab37b1f690c7 clarified init/begin_theory: no longer depend on thy_info.ML;
wenzelm
parents: 23884
diff changeset
   461
    val parents = Theory.parents_of thy;
ab37b1f690c7 clarified init/begin_theory: no longer depend on thy_info.ML;
wenzelm
parents: 23884
diff changeset
   462
    val parent_specs = map (parent_link remote_path path) parents;
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   463
37939
965537d86fcc discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents: 37216
diff changeset
   464
    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
   465
      let
43712
3c2c912af2ef moved Outer_Syntax.load_thy to Thy_Load.load_thy;
wenzelm
parents: 43437
diff changeset
   466
        val path = File.check_file (File.full_path dir raw_path);
37939
965537d86fcc discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents: 37216
diff changeset
   467
        val base = Path.base path;
965537d86fcc discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents: 37216
diff changeset
   468
        val base_html = html_ext base;
965537d86fcc discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents: 37216
diff changeset
   469
        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
   470
          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
   471
      in (Url.File base_html, Url.File raw_path, loadit) end);
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   472
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   473
    fun prep_html_source (tex_source, html_source, html) =
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   474
      let
14898
a25550451b51 Url.File;
wenzelm
parents: 14598
diff changeset
   475
        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
   476
          name parent_specs files_html (Buffer.content html_source)
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   477
      in (tex_source, Buffer.empty, Buffer.add txt html) end;
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   478
9416
9144976964e7 removed all_sessions.graph;
wenzelm
parents: 9136
diff changeset
   479
    val entry =
9144976964e7 removed all_sessions.graph;
wenzelm
parents: 9136
diff changeset
   480
     {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
   481
      path = Path.implode (html_path name),
23899
ab37b1f690c7 clarified init/begin_theory: no longer depend on thy_info.ML;
wenzelm
parents: 23884
diff changeset
   482
      parents = map ID_of_thy parents};
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   483
  in
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   484
    change_theory_info name prep_html_source;
24150
ed724867099a sort indexes according to symbolic update_time (multithreading-safe);
wenzelm
parents: 24102
diff changeset
   485
    add_graph_entry (update_time, entry);
ed724867099a sort indexes according to symbolic update_time (multithreading-safe);
wenzelm
parents: 24102
diff changeset
   486
    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
   487
    add_tex_index (update_time, Latex.theory_entry name);
27327
efd626efcb04 info: default name is "", not "Pure";
wenzelm
parents: 26957
diff changeset
   488
    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
   489
  end);
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   490
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   491
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   492
42127
8223e7f4b0da Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
wenzelm
parents: 42126
diff changeset
   493
(** draft document output **)
14922
88c1e108d0bf added Present.drafts;
wenzelm
parents: 14898
diff changeset
   494
42127
8223e7f4b0da Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
wenzelm
parents: 42126
diff changeset
   495
fun drafts doc_format src_paths = Isabelle_System.with_tmp_dir "drafts" (fn dir =>
14922
88c1e108d0bf added Present.drafts;
wenzelm
parents: 14898
diff changeset
   496
  let
24150
ed724867099a sort indexes according to symbolic update_time (multithreading-safe);
wenzelm
parents: 24102
diff changeset
   497
    fun prep_draft path i =
14935
c2441592be14 tuned Present.drafts;
wenzelm
parents: 14922
diff changeset
   498
      let
c2441592be14 tuned Present.drafts;
wenzelm
parents: 14922
diff changeset
   499
        val base = Path.base path;
14972
wenzelm
parents: 14967
diff changeset
   500
        val name =
24829
e1214fa781ca avoid gensym;
wenzelm
parents: 24561
diff changeset
   501
          (case Path.implode (#1 (Path.split_ext base)) of
e1214fa781ca avoid gensym;
wenzelm
parents: 24561
diff changeset
   502
            "" => "DUMMY" ^ serial_string ()
e1214fa781ca avoid gensym;
wenzelm
parents: 24561
diff changeset
   503
          | s => s);
14935
c2441592be14 tuned Present.drafts;
wenzelm
parents: 14922
diff changeset
   504
      in
c2441592be14 tuned Present.drafts;
wenzelm
parents: 14922
diff changeset
   505
        if File.exists path then
24150
ed724867099a sort indexes according to symbolic update_time (multithreading-safe);
wenzelm
parents: 24102
diff changeset
   506
          (((name, base, File.read path), (i, Latex.theory_entry name)), i + 1)
41944
b97091ae583a Path.print is the official way to show file-system paths to users -- note that Path.implode often indicates violation of the abstract datatype;
wenzelm
parents: 41886
diff changeset
   507
        else error ("Bad file: " ^ Path.print path)
14935
c2441592be14 tuned Present.drafts;
wenzelm
parents: 14922
diff changeset
   508
      end;
24150
ed724867099a sort indexes according to symbolic update_time (multithreading-safe);
wenzelm
parents: 24102
diff changeset
   509
    val (srcs, tex_index) = split_list (fst (fold_map prep_draft src_paths 0));
14935
c2441592be14 tuned Present.drafts;
wenzelm
parents: 14922
diff changeset
   510
42127
8223e7f4b0da Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
wenzelm
parents: 42126
diff changeset
   511
    val doc_path = Path.append dir document_path;
40743
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents: 39733
diff changeset
   512
    val _ = Isabelle_System.mkdirs doc_path;
14922
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;
40743
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents: 39733
diff changeset
   515
    val _ = Isabelle_System.isabelle_tool "latex" ("-o sty " ^ File.shell_path root_path);
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents: 39733
diff changeset
   516
    val _ = Isabelle_System.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;
88c1e108d0bf added Present.drafts;
wenzelm
parents: 14898
diff changeset
   529
42127
8223e7f4b0da Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
wenzelm
parents: 42126
diff changeset
   530
    val result = isabelle_document false doc_format documentN "" doc_path dir;
8223e7f4b0da Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
wenzelm
parents: 42126
diff changeset
   531
    val result' = Isabelle_System.create_tmp_path documentN doc_format;
8223e7f4b0da Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
wenzelm
parents: 42126
diff changeset
   532
    val _ = File.copy result result';
8223e7f4b0da Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
wenzelm
parents: 42126
diff changeset
   533
  in result' end);
14922
88c1e108d0bf added Present.drafts;
wenzelm
parents: 14898
diff changeset
   534
7685
3edd32d588a6 improved theory_source presentation (hook);
wenzelm
parents: 6325
diff changeset
   535
end;
3edd32d588a6 improved theory_source presentation (hook);
wenzelm
parents: 6325
diff changeset
   536
32738
15bb09ca0378 explicit indication of Unsynchronized.ref;
wenzelm
parents: 31819
diff changeset
   537
structure Basic_Present: BASIC_PRESENT = Present;
15bb09ca0378 explicit indication of Unsynchronized.ref;
wenzelm
parents: 31819
diff changeset
   538
open Basic_Present;