src/Pure/Thy/present.ML
author wenzelm
Sun, 28 Aug 2005 19:47:24 +0200
changeset 17177 53cc9e134f40
parent 17082 b0e9462db0b4
child 17210 e80fd664a119
permissions -rw-r--r--
isatool latex -o sty;
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
328b4377755c Theory presentation (fake implementation);
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
9416
9144976964e7 removed all_sessions.graph;
wenzelm
parents: 9136
diff changeset
     3
    Author:     Markus Wenzel and Stefan Berghofer, TU Muenchen
6203
328b4377755c Theory presentation (fake implementation);
wenzelm
parents:
diff changeset
     4
9416
9144976964e7 removed all_sessions.graph;
wenzelm
parents: 9136
diff changeset
     5
Theory presentation: HTML, graph files, (PDF)LaTeX documents.
6203
328b4377755c Theory presentation (fake implementation);
wenzelm
parents:
diff changeset
     6
*)
328b4377755c Theory presentation (fake implementation);
wenzelm
parents:
diff changeset
     7
328b4377755c Theory presentation (fake implementation);
wenzelm
parents:
diff changeset
     8
signature BASIC_PRESENT =
328b4377755c Theory presentation (fake implementation);
wenzelm
parents:
diff changeset
     9
sig
11057
e68becb804fe added no_document
wenzelm
parents: 9917
diff changeset
    10
  val no_document: ('a -> 'b) -> 'a -> 'b
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
    11
  val section: string -> unit
6203
328b4377755c Theory presentation (fake implementation);
wenzelm
parents:
diff changeset
    12
end;
328b4377755c Theory presentation (fake implementation);
wenzelm
parents:
diff changeset
    13
328b4377755c Theory presentation (fake implementation);
wenzelm
parents:
diff changeset
    14
signature PRESENT =
328b4377755c Theory presentation (fake implementation);
wenzelm
parents:
diff changeset
    15
sig
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
    16
  include BASIC_PRESENT
14922
88c1e108d0bf added Present.drafts;
wenzelm
parents: 14898
diff changeset
    17
  val get_info: theory -> {name: string, session: string list, is_local: bool}
9452
fc02c5bacaab export write_graph;
wenzelm
parents: 9416
diff changeset
    18
  val write_graph: {name: string, ID: string, dir: string, unfold: bool,
fc02c5bacaab export write_graph;
wenzelm
parents: 9416
diff changeset
    19
   path: string, parents: string list} list -> Path.T -> unit
17082
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
    20
  val init: bool -> bool -> string -> bool -> string list -> string list ->
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
    21
    string -> Path.T option -> Url.T option * bool -> bool -> 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
8192
45a7027136e3 added old_symbol_source;
wenzelm
parents: 8088
diff changeset
    24
  val verbatim_source: string -> (unit -> Symbol.symbol list) -> unit
45a7027136e3 added old_symbol_source;
wenzelm
parents: 8088
diff changeset
    25
  val old_symbol_source: string -> (unit -> Symbol.symbol list) -> unit
9136
8196955b02ec adapted to improved presentation;
wenzelm
parents: 9044
diff changeset
    26
  val theory_output: string -> string -> unit
15159
2ef19a680646 begin_theory now takes optional path (current directory) as argument.
berghofe
parents: 14981
diff changeset
    27
  val begin_theory: Path.T option -> string -> string list ->
2ef19a680646 begin_theory now takes optional path (current directory) as argument.
berghofe
parents: 14981
diff changeset
    28
    (Path.T * bool) list -> theory -> theory
13532
131bb248504d simplified results;
wenzelm
parents: 12898
diff changeset
    29
  val add_hook: (string -> (string * thm list) list -> unit) -> unit
131bb248504d simplified results;
wenzelm
parents: 12898
diff changeset
    30
  val results: string -> (string * thm list) list -> unit
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
    31
  val theorem: string -> thm -> unit
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
    32
  val theorems: string -> thm list -> unit
8088
6ae943d080de chapter;
wenzelm
parents: 7853
diff changeset
    33
  val chapter: string -> unit
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
    34
  val subsection: string -> unit
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
    35
  val subsubsection: string -> unit
14922
88c1e108d0bf added Present.drafts;
wenzelm
parents: 14898
diff changeset
    36
  val drafts: string -> Path.T list -> Path.T
6203
328b4377755c Theory presentation (fake implementation);
wenzelm
parents:
diff changeset
    37
end;
328b4377755c Theory presentation (fake implementation);
wenzelm
parents:
diff changeset
    38
7685
3edd32d588a6 improved theory_source presentation (hook);
wenzelm
parents: 6325
diff changeset
    39
structure Present: PRESENT =
3edd32d588a6 improved theory_source presentation (hook);
wenzelm
parents: 6325
diff changeset
    40
struct
3edd32d588a6 improved theory_source presentation (hook);
wenzelm
parents: 6325
diff changeset
    41
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
    42
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
    43
(** paths **)
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
    44
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
    45
val output_path = Path.variable "ISABELLE_BROWSER_INFO";
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
    46
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
    47
val tex_ext = Path.ext "tex";
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
    48
val tex_path = tex_ext o Path.basic;
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
    49
val html_ext = Path.ext "html";
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
    50
val html_path = html_ext o Path.basic;
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
    51
val index_path = Path.basic "index.html";
11856
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
    52
val readme_html_path = Path.basic "README.html";
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
    53
val readme_path = Path.basic "README";
17082
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
    54
val documentN = "document";
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
    55
val document_path = Path.basic documentN;
8196
ecb9decd38ac additional tex dump;
wenzelm
parents: 8192
diff changeset
    56
val doc_indexN = "session";
11856
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
    57
val graph_path = Path.basic "session.graph";
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
    58
val graph_pdf_path = Path.basic "session_graph.pdf";
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
    59
val graph_eps_path = Path.basic "session_graph.eps";
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
    60
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
    61
val session_path = Path.basic ".session";
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
    62
val session_entries_path = Path.unpack ".session/entries";
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
    63
val pre_index_path = Path.unpack ".session/pre-index";
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
    64
9044
28ee037278a6 Reorganized graph stuff.
berghofe
parents: 8808
diff changeset
    65
fun mk_rel_path [] ys = Path.make ys
28ee037278a6 Reorganized graph stuff.
berghofe
parents: 8808
diff changeset
    66
  | mk_rel_path xs [] = Path.appends (replicate (length xs) Path.parent)
9416
9144976964e7 removed all_sessions.graph;
wenzelm
parents: 9136
diff changeset
    67
  | 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
    68
      Path.appends (replicate (length ps) Path.parent @ [Path.make qs]);
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
    69
11856
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
    70
fun show_path path = Path.pack (Path.append (File.pwd ()) path);
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
    71
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
    72
14922
88c1e108d0bf added Present.drafts;
wenzelm
parents: 14898
diff changeset
    73
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
    74
(** additional theory data **)
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
    75
16426
8c3118c9c054 accomodate change of TheoryDataFun;
wenzelm
parents: 16263
diff changeset
    76
structure BrowserInfoData = TheoryDataFun
8c3118c9c054 accomodate change of TheoryDataFun;
wenzelm
parents: 16263
diff changeset
    77
(struct
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
    78
  val name = "Pure/browser_info";
9416
9144976964e7 removed all_sessions.graph;
wenzelm
parents: 9136
diff changeset
    79
  type T = {name: string, session: string list, is_local: bool};
16503
24491bde68df clarify empty vs. pure browser info;
wenzelm
parents: 16426
diff changeset
    80
  val empty = {name = "", session = [], is_local = false}: T;
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
    81
  val copy = I;
16503
24491bde68df clarify empty vs. pure browser info;
wenzelm
parents: 16426
diff changeset
    82
  fun extend _ = empty;
16426
8c3118c9c054 accomodate change of TheoryDataFun;
wenzelm
parents: 16263
diff changeset
    83
  fun merge _ _ = empty;
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
    84
  fun print _ _ = ();
16426
8c3118c9c054 accomodate change of TheoryDataFun;
wenzelm
parents: 16263
diff changeset
    85
end);
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
    86
15801
d2f5ca3c048d superceded by Pure.thy and CPure.thy;
wenzelm
parents: 15570
diff changeset
    87
val _ = Context.add_setup [BrowserInfoData.init];
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
    88
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
    89
fun get_info thy =
16426
8c3118c9c054 accomodate change of TheoryDataFun;
wenzelm
parents: 16263
diff changeset
    90
  if Context.theory_name thy mem_string [Context.ProtoPureN, Context.PureN, Context.CPureN]
16503
24491bde68df clarify empty vs. pure browser info;
wenzelm
parents: 16426
diff changeset
    91
  then {name = Context.PureN, session = [], is_local = false}
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
    92
  else BrowserInfoData.get thy;
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
    93
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
    94
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
    95
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
    96
(** graphs **)
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
    97
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
    98
type graph_node =
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
    99
  {name: string, ID: string, dir: string, unfold: bool,
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   100
   path: string, parents: string list};
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   101
9416
9144976964e7 removed all_sessions.graph;
wenzelm
parents: 9136
diff changeset
   102
fun write_graph gr path =
9144976964e7 removed all_sessions.graph;
wenzelm
parents: 9136
diff changeset
   103
  File.write path (cat_lines (map (fn {name, ID, dir, unfold, path, parents} =>
9144976964e7 removed all_sessions.graph;
wenzelm
parents: 9136
diff changeset
   104
    "\"" ^ name ^ "\" \"" ^ ID ^ "\" \"" ^ dir ^ (if unfold then "\" + \"" else "\" \"") ^
14598
7009f59711e3 Replaced quote by Library.quote, since quote now refers to Symbol.quote
berghofe
parents: 14540
diff changeset
   105
    path ^ "\" > " ^ space_implode " " (map Library.quote parents) ^ " ;") gr));
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   106
9416
9144976964e7 removed all_sessions.graph;
wenzelm
parents: 9136
diff changeset
   107
fun ID_of sess s = space_implode "/" (sess @ [s]);
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   108
9416
9144976964e7 removed all_sessions.graph;
wenzelm
parents: 9136
diff changeset
   109
(*retrieve graph data from initial theory loader database*)
9144976964e7 removed all_sessions.graph;
wenzelm
parents: 9136
diff changeset
   110
fun init_graph remote_path curr_sess = map (fn name =>
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   111
  let
9416
9144976964e7 removed all_sessions.graph;
wenzelm
parents: 9136
diff changeset
   112
    val {name = sess_name, session, is_local} = get_info (ThyInfo.theory name);
9144976964e7 removed all_sessions.graph;
wenzelm
parents: 9136
diff changeset
   113
    val path' = Path.append (Path.make session) (html_path name);
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   114
  in
9416
9144976964e7 removed all_sessions.graph;
wenzelm
parents: 9136
diff changeset
   115
   {name = name, ID = ID_of session name, dir = sess_name,
9144976964e7 removed all_sessions.graph;
wenzelm
parents: 9136
diff changeset
   116
    path =
9144976964e7 removed all_sessions.graph;
wenzelm
parents: 9136
diff changeset
   117
      if null session then "" else
16263
0609fb8df4a7 removed copy, copy_all (superceded by File.copy, File.copy_dir);
wenzelm
parents: 15801
diff changeset
   118
      if is_some remote_path andalso not is_local then
0609fb8df4a7 removed copy, copy_all (superceded by File.copy, File.copy_dir);
wenzelm
parents: 15801
diff changeset
   119
        Url.pack (Url.append (the remote_path) (Url.File
9416
9144976964e7 removed all_sessions.graph;
wenzelm
parents: 9136
diff changeset
   120
          (Path.append (Path.make session) (html_path name))))
9144976964e7 removed all_sessions.graph;
wenzelm
parents: 9136
diff changeset
   121
      else Path.pack (Path.append (mk_rel_path curr_sess session) (html_path name)),
9144976964e7 removed all_sessions.graph;
wenzelm
parents: 9136
diff changeset
   122
    unfold = false,
9144976964e7 removed all_sessions.graph;
wenzelm
parents: 9136
diff changeset
   123
    parents =
9144976964e7 removed all_sessions.graph;
wenzelm
parents: 9136
diff changeset
   124
      map (fn s => ID_of (#session (get_info (ThyInfo.theory s))) s) (ThyInfo.get_preds name)}
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   125
  end) (ThyInfo.names ());
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   126
9416
9144976964e7 removed all_sessions.graph;
wenzelm
parents: 9136
diff changeset
   127
fun ins_graph_entry (entry as {ID, ...}) (gr: graph_node list) =
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   128
  filter_out (fn entry' => #ID entry' = ID) gr @ [entry];
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   129
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   130
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   131
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   132
(** global browser info state **)
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   133
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   134
(* type theory_info *)
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   135
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   136
type theory_info = {tex_source: Buffer.T, html_source: Buffer.T, html: Buffer.T};
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   137
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   138
fun make_theory_info (tex_source, html_source, html) =
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   139
  {tex_source = tex_source, html_source = html_source, html = html}: theory_info;
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   140
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   141
val empty_theory_info = make_theory_info (Buffer.empty, Buffer.empty, Buffer.empty);
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   142
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   143
fun map_theory_info f {tex_source, html_source, html} =
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   144
  make_theory_info (f (tex_source, html_source, html));
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   145
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   146
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   147
(* type browser_info *)
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   148
11856
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
   149
type browser_info = {theories: theory_info Symtab.table, files: (Path.T * string) list,
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
   150
  tex_index: Buffer.T, html_index: Buffer.T, graph: graph_node list};
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   151
11856
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
   152
fun make_browser_info (theories, files, tex_index, html_index, graph) =
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
   153
  {theories = theories, files = files, tex_index = tex_index, html_index = html_index,
9416
9144976964e7 removed all_sessions.graph;
wenzelm
parents: 9136
diff changeset
   154
    graph = graph}: browser_info;
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   155
11856
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
   156
val empty_browser_info = make_browser_info (Symtab.empty, [], Buffer.empty, Buffer.empty, []);
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   157
9416
9144976964e7 removed all_sessions.graph;
wenzelm
parents: 9136
diff changeset
   158
fun init_browser_info remote_path curr_sess = make_browser_info
11856
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
   159
  (Symtab.empty, [], Buffer.empty, Buffer.empty, init_graph remote_path curr_sess);
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   160
11856
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
   161
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
   162
  make_browser_info (f (theories, files, tex_index, html_index, graph));
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   163
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   164
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   165
(* state *)
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   166
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   167
val browser_info = ref empty_browser_info;
11057
e68becb804fe added no_document
wenzelm
parents: 9917
diff changeset
   168
fun change_browser_info f = browser_info := map_browser_info f (! browser_info);
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   169
11057
e68becb804fe added no_document
wenzelm
parents: 9917
diff changeset
   170
val suppress_tex_source = ref false;
e68becb804fe added no_document
wenzelm
parents: 9917
diff changeset
   171
fun no_document f x = Library.setmp suppress_tex_source true f x;
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   172
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   173
fun init_theory_info name info =
11856
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
   174
  change_browser_info (fn (theories, files, tex_index, html_index, graph) =>
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
   175
    (Symtab.update ((name, info), theories), files, tex_index, html_index, graph));
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   176
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   177
fun change_theory_info name f =
11856
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
   178
  change_browser_info (fn (info as (theories, files, tex_index, html_index, graph)) =>
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   179
    (case Symtab.lookup (theories, name) of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15159
diff changeset
   180
      NONE => (warning ("Browser info: cannot access theory document " ^ quote name); info)
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15159
diff changeset
   181
    | SOME info => (Symtab.update ((name, map_theory_info f info), theories), files,
9416
9144976964e7 removed all_sessions.graph;
wenzelm
parents: 9136
diff changeset
   182
        tex_index, html_index, graph)));
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   183
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   184
11856
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
   185
fun add_file file =
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
   186
  change_browser_info (fn (theories, files, tex_index, html_index, graph) =>
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
   187
    (theories, file :: files, tex_index, html_index, graph));
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
   188
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   189
fun add_tex_index txt =
11856
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
   190
  change_browser_info (fn (theories, files, tex_index, html_index, graph) =>
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
   191
    (theories, files, Buffer.add txt tex_index, html_index, graph));
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   192
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   193
fun add_html_index txt =
11856
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
   194
  change_browser_info (fn (theories, files, tex_index, html_index, graph) =>
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
   195
    (theories, files, tex_index, Buffer.add txt html_index, graph));
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   196
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   197
fun add_graph_entry e =
11856
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
   198
  change_browser_info (fn (theories, files, tex_index, html_index, graph) =>
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
   199
    (theories, files, tex_index, html_index, ins_graph_entry e graph));
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   200
11057
e68becb804fe added no_document
wenzelm
parents: 9917
diff changeset
   201
fun add_tex_source name txt =
e68becb804fe added no_document
wenzelm
parents: 9917
diff changeset
   202
  if ! suppress_tex_source then ()
e68becb804fe added no_document
wenzelm
parents: 9917
diff changeset
   203
  else change_theory_info name (fn (tex_source, html_source, html) =>
e68becb804fe added no_document
wenzelm
parents: 9917
diff changeset
   204
    (Buffer.add txt tex_source, html_source, html));
7727
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_source 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, Buffer.add txt html_source, html));
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   208
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   209
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
   210
  (tex_source, html_source, Buffer.add txt html));
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   211
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   212
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   213
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   214
(** global session state **)
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   215
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   216
(* session_info *)
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   217
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   218
type session_info =
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   219
  {name: string, parent: string, session: string, path: string list, html_prefix: Path.T,
17082
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   220
    info: bool, doc_format: string, doc_graph: bool, documents: (string * string) list,
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   221
    doc_prefix1: (Path.T * Path.T) option, doc_prefix2: Path.T option, remote_path: Url.T option,
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   222
    verbose: bool, readme: Path.T option};
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   223
9416
9144976964e7 removed all_sessions.graph;
wenzelm
parents: 9136
diff changeset
   224
fun make_session_info
17082
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   225
  (name, parent, session, path, html_prefix, info, doc_format, doc_graph, documents,
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   226
    doc_prefix1, doc_prefix2, remote_path, verbose, readme) =
7802
fba7a36e8556 isatool_document;
wenzelm
parents: 7789
diff changeset
   227
  {name = name, parent = parent, session = session, path = path, html_prefix = html_prefix,
17082
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   228
    info = info, doc_format = doc_format, doc_graph = doc_graph, documents = documents,
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   229
    doc_prefix1 = doc_prefix1, doc_prefix2 = doc_prefix2, remote_path = remote_path,
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   230
    verbose = verbose, readme = readme}: session_info;
7685
3edd32d588a6 improved theory_source presentation (hook);
wenzelm
parents: 6325
diff changeset
   231
3edd32d588a6 improved theory_source presentation (hook);
wenzelm
parents: 6325
diff changeset
   232
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   233
(* state *)
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   234
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15159
diff changeset
   235
val session_info = ref (NONE: session_info option);
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   236
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15159
diff changeset
   237
fun with_session x f = (case ! session_info of NONE => x | SOME info => f info);
16426
8c3118c9c054 accomodate change of TheoryDataFun;
wenzelm
parents: 16263
diff changeset
   238
fun with_context f = f (Context.theory_name (Context.the_context ()));
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   239
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   240
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   241
14922
88c1e108d0bf added Present.drafts;
wenzelm
parents: 14898
diff changeset
   242
(** document preparation **)
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   243
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   244
(* maintain index *)
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   245
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   246
val session_entries =
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   247
  HTML.session_entries o
14898
a25550451b51 Url.File;
wenzelm
parents: 14598
diff changeset
   248
    map (fn name => (Url.File (Path.append (Path.basic name) index_path), name));
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   249
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   250
fun get_entries dir =
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   251
  split_lines (File.read (Path.append dir session_entries_path));
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   252
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   253
fun put_entries entries dir =
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   254
  File.write (Path.append dir session_entries_path) (cat_lines entries);
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   255
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   256
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   257
fun create_index dir =
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   258
  File.read (Path.append dir pre_index_path) ^
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   259
    session_entries (get_entries dir) ^ HTML.end_index
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   260
  |> File.write (Path.append dir index_path);
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   261
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   262
fun update_index dir name =
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   263
  (case try get_entries dir of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15159
diff changeset
   264
    NONE => warning ("Browser info: cannot access session index of " ^ quote (Path.pack dir))
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15159
diff changeset
   265
  | SOME es => (put_entries ((es \ name) @ [name]) dir; create_index dir));
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   266
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   267
17082
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   268
(* document versions *)
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   269
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   270
fun read_version str =
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   271
  (case space_explode "=" str of
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   272
    [name] => (name, "")
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   273
  | [name, tags] => (name, tags)
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   274
  | _ => error ("Malformed document version specification: " ^ quote str));
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   275
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   276
fun read_versions strs =
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   277
  rev (gen_distinct eq_fst (rev ((documentN, "") :: map read_version strs)))
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   278
  |> filter_out (equal "-" o #2);
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   279
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   280
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   281
(* init session *)
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   282
12895
d9dd528ecea6 clarified copy_all;
wenzelm
parents: 12849
diff changeset
   283
fun name_of_session elems = space_implode "/" ("Isabelle" :: elems);
d9dd528ecea6 clarified copy_all;
wenzelm
parents: 12849
diff changeset
   284
17082
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   285
fun init build info doc doc_graph doc_versions path name doc_prefix2
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   286
    (remote_path, first_time) verbose =
11911
6533ceee4cd7 build option enables most basic browser info (for proper recording of session);
wenzelm
parents: 11856
diff changeset
   287
  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
   288
    (browser_info := empty_browser_info; session_info := NONE)
11856
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
   289
  else
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
   290
    let
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
   291
      val parent_name = name_of_session (Library.take (length path - 1, path));
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
   292
      val session_name = name_of_session path;
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
   293
      val sess_prefix = Path.make path;
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
   294
      val html_prefix = Path.append (Path.expand output_path) sess_prefix;
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   295
17082
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   296
      val (doc_prefix1, documents) =
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   297
        if doc = "" then (NONE, [])
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   298
        else if not (File.exists document_path) then (conditional verbose (fn () =>
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   299
          std_error "Warning: missing document directory\n"); (NONE, []))
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   300
        else (SOME (Path.append html_prefix document_path, html_prefix),
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   301
          read_versions doc_versions);
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   302
11856
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
   303
      val parent_index_path = Path.append Path.parent index_path;
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
   304
      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
   305
          Url.append (the remote_path) (Url.File (Path.append sess_prefix parent_index_path))
14898
a25550451b51 Url.File;
wenzelm
parents: 14598
diff changeset
   306
        else Url.File parent_index_path;
11856
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
   307
      val readme =
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15159
diff changeset
   308
        if File.exists readme_html_path then SOME readme_html_path
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15159
diff changeset
   309
        else if File.exists readme_path then SOME readme_path
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15159
diff changeset
   310
        else NONE;
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   311
17082
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   312
      val docs =
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   313
        (case readme of NONE => [] | SOME p => [(Url.File p, "README")]) @
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   314
        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
   315
      val index_text = HTML.begin_index (index_up_lnk, parent_name)
17082
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   316
        (Url.File index_path, session_name) docs (Url.unpack "medium.html");
11856
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
   317
    in
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15159
diff changeset
   318
      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
   319
      info, doc, doc_graph, documents, doc_prefix1, doc_prefix2, remote_path, verbose, readme));
11856
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
   320
      browser_info := init_browser_info remote_path path;
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
   321
      add_html_index index_text
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
   322
    end;
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   323
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   324
17082
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   325
(* isatool wrappers *)
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   326
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   327
fun isatool_document verbose format name tags path result_path =
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   328
  let
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   329
    val s = "\"$ISATOOL\" document -c -o '" ^ format ^ "' \
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   330
      \-n '" ^ name ^ "' -t '" ^ tags ^ "' " ^ File.shell_path path ^
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   331
      " 2>&1" ^ (if verbose then "" else " >/dev/null");
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   332
    val doc_path = Path.append result_path (Path.ext format (Path.basic name));
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   333
  in
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   334
    conditional verbose (fn () => writeln s);
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   335
    system s;
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   336
    conditional (not (File.exists doc_path)) (fn () =>
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   337
      error ("No document: " ^ quote (show_path doc_path)));
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   338
    doc_path
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   339
  end;
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   340
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   341
fun isatool_browser graph =
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   342
  let
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   343
    val pdf_path = File.tmp_path graph_pdf_path;
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   344
    val eps_path = File.tmp_path graph_eps_path;
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   345
    val gr_path = File.tmp_path graph_path;
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   346
    val s = "browser -o " ^ File.shell_path pdf_path ^ " " ^ File.shell_path gr_path;
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   347
  in
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   348
    write_graph graph gr_path;
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   349
    if File.isatool s <> 0 orelse not (File.exists eps_path) orelse not (File.exists pdf_path)
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   350
    then error "Failed to prepare dependency graph"
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   351
    else
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   352
      let val pdf = File.read pdf_path and eps = File.read eps_path
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   353
      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
   354
  end;
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   355
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   356
11856
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
   357
(* finish session -- output all generated text *)
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
   358
14922
88c1e108d0bf added Present.drafts;
wenzelm
parents: 14898
diff changeset
   359
fun write_tex src name path =
88c1e108d0bf added Present.drafts;
wenzelm
parents: 14898
diff changeset
   360
  Buffer.write (Path.append path (tex_path name)) src;
88c1e108d0bf added Present.drafts;
wenzelm
parents: 14898
diff changeset
   361
88c1e108d0bf added Present.drafts;
wenzelm
parents: 14898
diff changeset
   362
fun write_tex_index tex_index path =
88c1e108d0bf added Present.drafts;
wenzelm
parents: 14898
diff changeset
   363
  write_tex (Buffer.add Latex.tex_trailer tex_index) doc_indexN path;
88c1e108d0bf added Present.drafts;
wenzelm
parents: 14898
diff changeset
   364
7685
3edd32d588a6 improved theory_source presentation (hook);
wenzelm
parents: 6325
diff changeset
   365
11856
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
   366
fun finish () = with_session () (fn {name, info, html_prefix, doc_format, doc_graph,
17082
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   367
    documents, doc_prefix1, doc_prefix2, path, verbose, readme, ...} =>
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   368
  let
11856
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
   369
    val {theories, files, tex_index, html_index, graph} = ! browser_info;
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
   370
    val thys = Symtab.dest theories;
9416
9144976964e7 removed all_sessions.graph;
wenzelm
parents: 9136
diff changeset
   371
    val parent_html_prefix = Path.append html_prefix Path.parent;
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   372
11856
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
   373
    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
   374
    fun finish_html (a, {html, ...}: theory_info) =
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
   375
      Buffer.write (Path.append html_prefix (html_path a)) (Buffer.add HTML.end_theory html);
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
   376
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
   377
    val opt_graphs =
16263
0609fb8df4a7 removed copy, copy_all (superceded by File.copy, File.copy_dir);
wenzelm
parents: 15801
diff changeset
   378
      if doc_graph andalso (is_some doc_prefix1 orelse is_some doc_prefix2) then
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15159
diff changeset
   379
        SOME (isatool_browser graph)
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15159
diff changeset
   380
      else NONE;
11856
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
   381
12895
d9dd528ecea6 clarified copy_all;
wenzelm
parents: 12849
diff changeset
   382
    fun prepare_sources path =
16263
0609fb8df4a7 removed copy, copy_all (superceded by File.copy, File.copy_dir);
wenzelm
parents: 15801
diff changeset
   383
     (File.mkdir path;
17082
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   384
      File.copy_dir document_path path;
17177
53cc9e134f40 isatool latex -o sty;
wenzelm
parents: 17082
diff changeset
   385
      File.isatool ("latex -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);
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   391
  in
11856
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
   392
    conditional info (fn () =>
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
   393
     (File.mkdir (Path.append html_prefix session_path);
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
   394
      Buffer.write (Path.append html_prefix pre_index_path) html_index;
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
   395
      File.write (Path.append html_prefix session_entries_path) "";
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
   396
      create_index html_prefix;
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
   397
      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
   398
      (case readme of NONE => () | SOME path => File.copy path html_prefix);
11856
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
   399
      write_graph graph (Path.append html_prefix graph_path);
16263
0609fb8df4a7 removed copy, copy_all (superceded by File.copy, File.copy_dir);
wenzelm
parents: 15801
diff changeset
   400
      File.copy (Path.unpack "~~/lib/browser/GraphBrowser.jar") html_prefix;
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   401
      List.app (fn (a, txt) => File.write (Path.append html_prefix (Path.basic a)) txt)
14898
a25550451b51 Url.File;
wenzelm
parents: 14598
diff changeset
   402
        (HTML.applet_pages name (Url.File index_path, name));
16263
0609fb8df4a7 removed copy, copy_all (superceded by File.copy, File.copy_dir);
wenzelm
parents: 15801
diff changeset
   403
      File.copy (Path.unpack "~~/lib/html/isabelle.css") html_prefix;
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   404
      List.app finish_html thys;
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   405
      List.app (uncurry File.write) files;
11856
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
   406
      conditional verbose (fn () =>
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
   407
        std_error ("Browser info at " ^ show_path html_prefix ^ "\n"))));
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
   408
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15159
diff changeset
   409
    (case doc_prefix2 of NONE => () | SOME path =>
12895
d9dd528ecea6 clarified copy_all;
wenzelm
parents: 12849
diff changeset
   410
     (prepare_sources path;
d9dd528ecea6 clarified copy_all;
wenzelm
parents: 12849
diff changeset
   411
      conditional verbose (fn () => std_error ("Document sources at " ^ show_path path ^ "\n"))));
d9dd528ecea6 clarified copy_all;
wenzelm
parents: 12849
diff changeset
   412
17082
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   413
    (case doc_prefix1 of NONE => () | SOME (path, result_path) =>
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   414
      documents |> List.app (fn (name, tags) =>
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   415
       let
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   416
         val _ = prepare_sources path;
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   417
         val doc_path = isatool_document true doc_format name tags path result_path;
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   418
       in
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   419
         conditional verbose (fn () => std_error ("Document at " ^ show_path doc_path ^ "\n"))
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   420
       end));
11856
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
   421
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   422
    browser_info := empty_browser_info;
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15159
diff changeset
   423
    session_info := NONE
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   424
  end);
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   425
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   426
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   427
(* theory elements *)
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   428
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   429
fun init_theory name = with_session () (fn _ => init_theory_info name empty_theory_info);
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   430
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   431
fun verbatim_source name mk_text =
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   432
  with_session () (fn _ => add_html_source name (HTML.verbatim_source (mk_text ())));
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   433
8192
45a7027136e3 added old_symbol_source;
wenzelm
parents: 8088
diff changeset
   434
fun old_symbol_source name mk_text =
14922
88c1e108d0bf added Present.drafts;
wenzelm
parents: 14898
diff changeset
   435
  with_session () (fn _ => add_tex_source name
88c1e108d0bf added Present.drafts;
wenzelm
parents: 14898
diff changeset
   436
    (Latex.symbol_source (K true, K true) name (mk_text ())));
8192
45a7027136e3 added old_symbol_source;
wenzelm
parents: 8088
diff changeset
   437
9136
8196955b02ec adapted to improved presentation;
wenzelm
parents: 9044
diff changeset
   438
fun theory_output name s =
9917
5af7632388a0 support \isabellecontext;
wenzelm
parents: 9795
diff changeset
   439
  with_session () (fn _ => add_tex_source name (Latex.isabelle_file name s));
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   440
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   441
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   442
fun parent_link remote_path curr_session name =
9416
9144976964e7 removed all_sessions.graph;
wenzelm
parents: 9136
diff changeset
   443
  let val {name = _, session, is_local} = get_info (ThyInfo.theory name)
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15159
diff changeset
   444
  in (if null session then NONE else
16263
0609fb8df4a7 removed copy, copy_all (superceded by File.copy, File.copy_dir);
wenzelm
parents: 15801
diff changeset
   445
     SOME (if is_some remote_path andalso not is_local then
0609fb8df4a7 removed copy, copy_all (superceded by File.copy, File.copy_dir);
wenzelm
parents: 15801
diff changeset
   446
       Url.append (the remote_path) (Url.File
9044
28ee037278a6 Reorganized graph stuff.
berghofe
parents: 8808
diff changeset
   447
         (Path.append (Path.make session) (html_path name)))
14898
a25550451b51 Url.File;
wenzelm
parents: 14598
diff changeset
   448
     else Url.File (Path.append (mk_rel_path curr_session session)
9044
28ee037278a6 Reorganized graph stuff.
berghofe
parents: 8808
diff changeset
   449
       (html_path name))), name)
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   450
  end;
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   451
15159
2ef19a680646 begin_theory now takes optional path (current directory) as argument.
berghofe
parents: 14981
diff changeset
   452
fun begin_theory optpath name raw_parents orig_files thy =
9416
9144976964e7 removed all_sessions.graph;
wenzelm
parents: 9136
diff changeset
   453
    with_session thy (fn {name = sess_name, session, path, html_prefix, remote_path, ...} =>
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   454
  let
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   455
    val parents = map (parent_link remote_path path) raw_parents;
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   456
    val ml_path = ThyLoad.ml_path name;
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15159
diff changeset
   457
    val files = map (apsnd SOME) orig_files @
16263
0609fb8df4a7 removed copy, copy_all (superceded by File.copy, File.copy_dir);
wenzelm
parents: 15801
diff changeset
   458
      (if is_some (ThyLoad.check_file optpath ml_path) then [(ml_path, NONE)] else []);
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   459
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   460
    fun prep_file (raw_path, loadit) =
15159
2ef19a680646 begin_theory now takes optional path (current directory) as argument.
berghofe
parents: 14981
diff changeset
   461
      (case ThyLoad.check_file optpath raw_path of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15159
diff changeset
   462
        SOME (path, _) =>
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   463
          let
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   464
            val base = Path.base path;
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   465
            val base_html = html_ext base;
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   466
          in
11856
a35af478aee4 graceful interpretation of -i/-d/-D options;
wenzelm
parents: 11580
diff changeset
   467
            add_file (Path.append html_prefix base_html,
14898
a25550451b51 Url.File;
wenzelm
parents: 14598
diff changeset
   468
              HTML.ml_file (Url.File base) (File.read path));
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15159
diff changeset
   469
            (SOME (Url.File base_html), Url.File raw_path, loadit)
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   470
          end
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15159
diff changeset
   471
      | NONE => (warning ("Browser info: expected to find ML file" ^ quote (Path.pack raw_path));
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15159
diff changeset
   472
          (NONE, Url.File raw_path, loadit)));
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   473
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   474
    val files_html = map prep_file files;
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   475
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   476
    fun prep_html_source (tex_source, html_source, html) =
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   477
      let
14898
a25550451b51 Url.File;
wenzelm
parents: 14598
diff changeset
   478
        val txt = HTML.begin_theory (Url.File index_path, session)
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   479
          name parents files_html (Buffer.content html_source)
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   480
      in (tex_source, Buffer.empty, Buffer.add txt html) end;
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   481
9416
9144976964e7 removed all_sessions.graph;
wenzelm
parents: 9136
diff changeset
   482
    val entry =
9144976964e7 removed all_sessions.graph;
wenzelm
parents: 9136
diff changeset
   483
     {name = name, ID = ID_of path name, dir = sess_name, unfold = true,
9144976964e7 removed all_sessions.graph;
wenzelm
parents: 9136
diff changeset
   484
      path = Path.pack (html_path name),
9144976964e7 removed all_sessions.graph;
wenzelm
parents: 9136
diff changeset
   485
      parents = map (fn s => ID_of (#session (get_info (ThyInfo.theory s))) s) raw_parents};
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   486
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   487
  in
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   488
    change_theory_info name prep_html_source;
9416
9144976964e7 removed all_sessions.graph;
wenzelm
parents: 9136
diff changeset
   489
    add_graph_entry entry;
14898
a25550451b51 Url.File;
wenzelm
parents: 14598
diff changeset
   490
    add_html_index (HTML.theory_entry (Url.File (html_path name), name));
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   491
    add_tex_index (Latex.theory_entry name);
16263
0609fb8df4a7 removed copy, copy_all (superceded by File.copy, File.copy_dir);
wenzelm
parents: 15801
diff changeset
   492
    BrowserInfoData.put {name = sess_name, session = path, is_local = is_some remote_path} thy
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   493
  end);
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   494
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   495
13532
131bb248504d simplified results;
wenzelm
parents: 12898
diff changeset
   496
val hooks = ref ([]: (string -> (string * thm list) list -> unit) list);
131bb248504d simplified results;
wenzelm
parents: 12898
diff changeset
   497
fun add_hook f = hooks := (f :: ! hooks);
131bb248504d simplified results;
wenzelm
parents: 12898
diff changeset
   498
131bb248504d simplified results;
wenzelm
parents: 12898
diff changeset
   499
fun results k xs =
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   500
 (List.app (fn f => (try (fn () => f k xs) (); ())) (! hooks);
13532
131bb248504d simplified results;
wenzelm
parents: 12898
diff changeset
   501
  with_session () (fn _ => with_context add_html (HTML.results k xs)));
131bb248504d simplified results;
wenzelm
parents: 12898
diff changeset
   502
131bb248504d simplified results;
wenzelm
parents: 12898
diff changeset
   503
fun theorem a th = results "theorem" [(a, [th])];
131bb248504d simplified results;
wenzelm
parents: 12898
diff changeset
   504
fun theorems a ths = results "theorems" [(a, ths)];
8088
6ae943d080de chapter;
wenzelm
parents: 7853
diff changeset
   505
fun chapter s = with_session () (fn _ => with_context add_html (HTML.chapter s));
7727
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   506
fun section s = with_session () (fn _ => with_context add_html (HTML.section s));
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   507
fun subsection s = with_session () (fn _ => with_context add_html (HTML.subsection s));
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   508
fun subsubsection s = with_session () (fn _ => with_context add_html (HTML.subsubsection s));
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   509
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   510
b52c7d773121 include browser_info stuff;
wenzelm
parents: 7685
diff changeset
   511
14922
88c1e108d0bf added Present.drafts;
wenzelm
parents: 14898
diff changeset
   512
(** draft document output **)
88c1e108d0bf added Present.drafts;
wenzelm
parents: 14898
diff changeset
   513
88c1e108d0bf added Present.drafts;
wenzelm
parents: 14898
diff changeset
   514
fun drafts doc_format src_paths =
88c1e108d0bf added Present.drafts;
wenzelm
parents: 14898
diff changeset
   515
  let
14935
c2441592be14 tuned Present.drafts;
wenzelm
parents: 14922
diff changeset
   516
    fun prep_draft (tex_index, path) =
c2441592be14 tuned Present.drafts;
wenzelm
parents: 14922
diff changeset
   517
      let
c2441592be14 tuned Present.drafts;
wenzelm
parents: 14922
diff changeset
   518
        val base = Path.base path;
14972
wenzelm
parents: 14967
diff changeset
   519
        val name =
wenzelm
parents: 14967
diff changeset
   520
          (case Path.pack (#1 (Path.split_ext base)) of "" => gensym "DUMMY" | s => s);
14935
c2441592be14 tuned Present.drafts;
wenzelm
parents: 14922
diff changeset
   521
      in
c2441592be14 tuned Present.drafts;
wenzelm
parents: 14922
diff changeset
   522
        if File.exists path then
c2441592be14 tuned Present.drafts;
wenzelm
parents: 14922
diff changeset
   523
          (Buffer.add (Latex.theory_entry name) tex_index, (name, base, File.read path))
c2441592be14 tuned Present.drafts;
wenzelm
parents: 14922
diff changeset
   524
        else error ("Bad file: " ^ quote (Path.pack path))
c2441592be14 tuned Present.drafts;
wenzelm
parents: 14922
diff changeset
   525
      end;
c2441592be14 tuned Present.drafts;
wenzelm
parents: 14922
diff changeset
   526
    val (tex_index, srcs) = foldl_map prep_draft (Buffer.empty, src_paths);
c2441592be14 tuned Present.drafts;
wenzelm
parents: 14922
diff changeset
   527
17082
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   528
    val doc_path = File.tmp_path document_path;
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   529
    val result_path = Path.append doc_path Path.parent;
14922
88c1e108d0bf added Present.drafts;
wenzelm
parents: 14898
diff changeset
   530
    val _ = File.mkdir doc_path;
88c1e108d0bf added Present.drafts;
wenzelm
parents: 14898
diff changeset
   531
    val root_path = Path.append doc_path (Path.basic "root.tex");
88c1e108d0bf added Present.drafts;
wenzelm
parents: 14898
diff changeset
   532
    val _ = File.copy (Path.unpack "~~/lib/texinputs/draft.tex") root_path;
16263
0609fb8df4a7 removed copy, copy_all (superceded by File.copy, File.copy_dir);
wenzelm
parents: 15801
diff changeset
   533
    val _ = File.isatool ("latex -o sty " ^ File.shell_path root_path);
0609fb8df4a7 removed copy, copy_all (superceded by File.copy, File.copy_dir);
wenzelm
parents: 15801
diff changeset
   534
    val _ = File.isatool ("latex -o syms " ^ File.shell_path root_path);
14922
88c1e108d0bf added Present.drafts;
wenzelm
parents: 14898
diff changeset
   535
88c1e108d0bf added Present.drafts;
wenzelm
parents: 14898
diff changeset
   536
    fun known name =
88c1e108d0bf added Present.drafts;
wenzelm
parents: 14898
diff changeset
   537
      let val ss = split_lines (File.read (Path.append doc_path (Path.basic name)))
88c1e108d0bf added Present.drafts;
wenzelm
parents: 14898
diff changeset
   538
      in fn s => s mem_string ss end;
88c1e108d0bf added Present.drafts;
wenzelm
parents: 14898
diff changeset
   539
    val known_syms = known "syms.lst";
88c1e108d0bf added Present.drafts;
wenzelm
parents: 14898
diff changeset
   540
    val known_ctrls = known "ctrls.lst";
88c1e108d0bf added Present.drafts;
wenzelm
parents: 14898
diff changeset
   541
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   542
    val _ = srcs |> List.app (fn (name, base, txt) =>
14935
c2441592be14 tuned Present.drafts;
wenzelm
parents: 14922
diff changeset
   543
      Symbol.explode txt
c2441592be14 tuned Present.drafts;
wenzelm
parents: 14922
diff changeset
   544
      |> Latex.symbol_source (known_syms, known_ctrls) (Path.pack base)
c2441592be14 tuned Present.drafts;
wenzelm
parents: 14922
diff changeset
   545
      |> File.write (Path.append doc_path (tex_path name)));
14922
88c1e108d0bf added Present.drafts;
wenzelm
parents: 14898
diff changeset
   546
    val _ = write_tex_index tex_index doc_path;
17082
b0e9462db0b4 support for document versions;
wenzelm
parents: 16503
diff changeset
   547
  in isatool_document false doc_format documentN "" doc_path result_path end;
14922
88c1e108d0bf added Present.drafts;
wenzelm
parents: 14898
diff changeset
   548
88c1e108d0bf added Present.drafts;
wenzelm
parents: 14898
diff changeset
   549
7685
3edd32d588a6 improved theory_source presentation (hook);
wenzelm
parents: 6325
diff changeset
   550
end;
3edd32d588a6 improved theory_source presentation (hook);
wenzelm
parents: 6325
diff changeset
   551
6203
328b4377755c Theory presentation (fake implementation);
wenzelm
parents:
diff changeset
   552
structure BasicPresent: BASIC_PRESENT = Present;
328b4377755c Theory presentation (fake implementation);
wenzelm
parents:
diff changeset
   553
open BasicPresent;