src/Pure/Thy/present.ML
author wenzelm
Wed Apr 15 19:08:37 2015 +0200 (2015-04-15)
changeset 60082 d3573eb7728f
parent 59448 149d2bc5ddb6
child 61372 cf40b6b1de54
permissions -rw-r--r--
session graph with folded base theories, as in document preparation;
wenzelm@6203
     1
(*  Title:      Pure/Thy/present.ML
wenzelm@9416
     2
    Author:     Markus Wenzel and Stefan Berghofer, TU Muenchen
wenzelm@6203
     3
wenzelm@59448
     4
Theory presentation: HTML and PDF-LaTeX documents.
wenzelm@6203
     5
*)
wenzelm@6203
     6
wenzelm@6203
     7
signature PRESENT =
wenzelm@6203
     8
sig
wenzelm@24561
     9
  val session_name: theory -> string
wenzelm@60082
    10
  val session_graph: string -> (string -> bool) -> theory -> Graph_Display.entry list
wenzelm@56614
    11
  val document_enabled: string -> bool
wenzelm@56612
    12
  val document_variants: string -> (string * string) list
wenzelm@59446
    13
  val init: bool -> bool -> Path.T -> string -> string -> (string * string) list ->
wenzelm@59448
    14
    (Path.T * Path.T) list -> Path.T -> string * string -> bool -> unit
wenzelm@59445
    15
  val finish: unit -> unit
wenzelm@9136
    16
  val theory_output: string -> string -> unit
wenzelm@54456
    17
  val begin_theory: int -> (unit -> HTML.text) -> theory -> theory
wenzelm@52549
    18
  val display_drafts: Path.T list -> int
wenzelm@6203
    19
end;
wenzelm@6203
    20
wenzelm@7685
    21
structure Present: PRESENT =
wenzelm@7685
    22
struct
wenzelm@7685
    23
wenzelm@7727
    24
wenzelm@7727
    25
(** paths **)
wenzelm@7727
    26
wenzelm@7727
    27
val tex_ext = Path.ext "tex";
wenzelm@7727
    28
val tex_path = tex_ext o Path.basic;
wenzelm@7727
    29
val html_ext = Path.ext "html";
wenzelm@7727
    30
val html_path = html_ext o Path.basic;
wenzelm@7727
    31
val index_path = Path.basic "index.html";
wenzelm@11856
    32
val readme_html_path = Path.basic "README.html";
wenzelm@17082
    33
val documentN = "document";
wenzelm@17082
    34
val document_path = Path.basic documentN;
wenzelm@8196
    35
val doc_indexN = "session";
wenzelm@59448
    36
val session_graph_path = Path.basic "session_graph.pdf";
wenzelm@7727
    37
wenzelm@51415
    38
fun show_path path = Path.implode (Path.expand (Path.append (File.pwd ()) path));
wenzelm@11856
    39
wenzelm@7727
    40
wenzelm@14922
    41
wenzelm@7727
    42
(** additional theory data **)
wenzelm@7727
    43
wenzelm@42008
    44
structure Browser_Info = Theory_Data
wenzelm@22846
    45
(
wenzelm@51399
    46
  type T = {chapter: string, name: string};
wenzelm@51567
    47
  val empty = {chapter = "Unsorted", name = "Unknown"}: T;
wenzelm@16503
    48
  fun extend _ = empty;
wenzelm@33522
    49
  fun merge _ = empty;
wenzelm@22846
    50
);
wenzelm@7727
    51
wenzelm@53171
    52
val _ = Theory.setup
wenzelm@53171
    53
  (Browser_Info.put {chapter = Context.PureN, name = Context.PureN});
wenzelm@51567
    54
wenzelm@51399
    55
val session_name = #name o Browser_Info.get;
wenzelm@7727
    56
wenzelm@7727
    57
wenzelm@60082
    58
(* session graph *)
wenzelm@60082
    59
wenzelm@60082
    60
fun session_graph parent_session parent_loaded =
wenzelm@60082
    61
  let
wenzelm@60082
    62
    val parent_session_name = "session." ^ parent_session;
wenzelm@60082
    63
    val parent_session_node = Graph_Display.content_node ("[" ^ parent_session ^ "]") [];
wenzelm@60082
    64
    fun node_name name = if parent_loaded name then parent_session_name else "theory." ^ name;
wenzelm@60082
    65
    fun theory_entry thy =
wenzelm@60082
    66
      let
wenzelm@60082
    67
        val name = Context.theory_name thy;
wenzelm@60082
    68
        val deps = map (node_name o Context.theory_name) (Theory.parents_of thy);
wenzelm@60082
    69
      in
wenzelm@60082
    70
        if parent_loaded name then NONE
wenzelm@60082
    71
        else SOME ((node_name name, Graph_Display.content_node name []), deps)
wenzelm@60082
    72
      end;
wenzelm@60082
    73
  in
wenzelm@60082
    74
    fn thy =>
wenzelm@60082
    75
      ((parent_session_name, parent_session_node), []) ::
wenzelm@60082
    76
        map_filter theory_entry (Theory.nodes_of thy)
wenzelm@60082
    77
  end;
wenzelm@60082
    78
wenzelm@60082
    79
wenzelm@7727
    80
wenzelm@7727
    81
(** global browser info state **)
wenzelm@7727
    82
wenzelm@7727
    83
(* type theory_info *)
wenzelm@7727
    84
wenzelm@54456
    85
type theory_info = {tex_source: string, html_source: string};
wenzelm@7727
    86
wenzelm@54456
    87
fun make_theory_info (tex_source, html_source) =
wenzelm@54456
    88
  {tex_source = tex_source, html_source = html_source}: theory_info;
wenzelm@7727
    89
wenzelm@54456
    90
fun map_theory_info f {tex_source, html_source} =
wenzelm@54456
    91
  make_theory_info (f (tex_source, html_source));
wenzelm@7727
    92
wenzelm@7727
    93
wenzelm@7727
    94
(* type browser_info *)
wenzelm@7727
    95
wenzelm@54455
    96
type browser_info =
wenzelm@54455
    97
 {theories: theory_info Symtab.table,
wenzelm@54455
    98
  tex_index: (int * string) list,
wenzelm@59448
    99
  html_index: (int * string) list};
wenzelm@7727
   100
wenzelm@59448
   101
fun make_browser_info (theories, tex_index, html_index) : browser_info =
wenzelm@59448
   102
  {theories = theories, tex_index = tex_index, html_index = html_index};
wenzelm@7727
   103
wenzelm@59448
   104
val empty_browser_info = make_browser_info (Symtab.empty, [], []);
wenzelm@7727
   105
wenzelm@59448
   106
fun map_browser_info f {theories, tex_index, html_index} =
wenzelm@59448
   107
  make_browser_info (f (theories, tex_index, html_index));
wenzelm@7727
   108
wenzelm@7727
   109
wenzelm@7727
   110
(* state *)
wenzelm@7727
   111
wenzelm@59173
   112
val browser_info = Synchronized.var "browser_info" empty_browser_info;
wenzelm@59173
   113
fun change_browser_info f = Synchronized.change browser_info (map_browser_info f);
wenzelm@7727
   114
wenzelm@7727
   115
fun init_theory_info name info =
wenzelm@59448
   116
  change_browser_info (fn (theories, tex_index, html_index) =>
wenzelm@59448
   117
    (Symtab.update (name, info) theories, tex_index, html_index));
wenzelm@7727
   118
wenzelm@7727
   119
fun change_theory_info name f =
wenzelm@59448
   120
  change_browser_info (fn (theories, tex_index, html_index) =>
wenzelm@17412
   121
    (case Symtab.lookup theories name of
wenzelm@27491
   122
      NONE => error ("Browser info: cannot access theory document " ^ quote name)
wenzelm@59448
   123
    | SOME info => (Symtab.update (name, map_theory_info f info) theories, tex_index, html_index)));
wenzelm@7727
   124
wenzelm@7727
   125
wenzelm@7727
   126
fun add_tex_index txt =
wenzelm@59448
   127
  change_browser_info (fn (theories, tex_index, html_index) =>
wenzelm@59448
   128
    (theories, txt :: tex_index, html_index));
wenzelm@7727
   129
wenzelm@7727
   130
fun add_html_index txt =
wenzelm@59448
   131
  change_browser_info (fn (theories, tex_index, html_index) =>
wenzelm@59448
   132
    (theories, tex_index, txt :: html_index));
wenzelm@7727
   133
wenzelm@7727
   134
wenzelm@7727
   135
wenzelm@7727
   136
(** global session state **)
wenzelm@7727
   137
wenzelm@7727
   138
(* session_info *)
wenzelm@7727
   139
wenzelm@7727
   140
type session_info =
wenzelm@59446
   141
  {name: string, chapter: string, info_path: Path.T, info: bool, doc_format: string,
wenzelm@59446
   142
    doc_output: Path.T option, doc_files: (Path.T * Path.T) list, graph_file: Path.T,
wenzelm@59446
   143
    documents: (string * string) list, verbose: bool, readme: Path.T option};
wenzelm@7727
   144
wenzelm@9416
   145
fun make_session_info
wenzelm@59446
   146
  (name, chapter, info_path, info, doc_format, doc_output, doc_files,
wenzelm@59446
   147
    graph_file, documents, verbose, readme) =
wenzelm@59446
   148
  {name = name, chapter = chapter, info_path = info_path, info = info, doc_format = doc_format,
wenzelm@59446
   149
    doc_output = doc_output, doc_files = doc_files, graph_file = graph_file,
wenzelm@59446
   150
    documents = documents, verbose = verbose, readme = readme}: session_info;
wenzelm@7685
   151
wenzelm@7685
   152
wenzelm@7727
   153
(* state *)
wenzelm@7727
   154
wenzelm@32738
   155
val session_info = Unsynchronized.ref (NONE: session_info option);
wenzelm@7727
   156
wenzelm@51399
   157
fun with_session_info x f = (case ! session_info of NONE => x | SOME info => f info);
wenzelm@7727
   158
wenzelm@7727
   159
wenzelm@7727
   160
wenzelm@14922
   161
(** document preparation **)
wenzelm@7727
   162
wenzelm@56614
   163
(* options *)
wenzelm@56614
   164
wenzelm@56614
   165
fun document_enabled s = s <> "" andalso s <> "false";
wenzelm@17082
   166
wenzelm@56612
   167
fun document_variants str =
wenzelm@56612
   168
  let
wenzelm@56612
   169
    fun read_variant s =
wenzelm@56612
   170
      (case space_explode "=" s of
wenzelm@56612
   171
        [name] => (name, "")
wenzelm@56612
   172
      | [name, tags] => (name, tags)
wenzelm@56612
   173
      | _ => error ("Malformed document variant specification: " ^ quote s));
wenzelm@56612
   174
    val variants = map read_variant (space_explode ":" str);
wenzelm@56612
   175
    val _ =
wenzelm@56612
   176
      (case duplicates (op =) (map #1 variants) of
wenzelm@56612
   177
        [] => ()
wenzelm@56612
   178
      | dups => error ("Duplicate document variants: " ^ commas_quote dups));
wenzelm@56612
   179
  in variants end;
wenzelm@17082
   180
wenzelm@17082
   181
wenzelm@7727
   182
(* init session *)
wenzelm@7727
   183
wenzelm@59446
   184
fun init build info info_path doc document_output doc_variants doc_files graph_file
wenzelm@59448
   185
    (chapter, name) verbose =
wenzelm@56530
   186
  if not build andalso not info andalso doc = "" then
wenzelm@59173
   187
    (Synchronized.change browser_info (K empty_browser_info); session_info := NONE)
wenzelm@11856
   188
  else
wenzelm@11856
   189
    let
wenzelm@51399
   190
      val doc_output =
wenzelm@51399
   191
        if document_output = "" then NONE else SOME (Path.explode document_output);
wenzelm@7727
   192
wenzelm@42007
   193
      val documents =
wenzelm@42007
   194
        if doc = "" then []
wenzelm@56533
   195
        else if null doc_files andalso not (can File.check_dir document_path) then
wenzelm@44389
   196
          (if verbose then Output.physical_stderr "Warning: missing document directory\n"
wenzelm@44389
   197
           else (); [])
wenzelm@48804
   198
        else doc_variants;
wenzelm@7727
   199
wenzelm@51419
   200
      val readme = if File.exists readme_html_path then SOME readme_html_path else NONE;
wenzelm@7727
   201
wenzelm@17082
   202
      val docs =
wenzelm@17082
   203
        (case readme of NONE => [] | SOME p => [(Url.File p, "README")]) @
wenzelm@42007
   204
          map (fn (name, _) => (Url.File (Path.ext doc (Path.basic name)), name)) documents;
wenzelm@11856
   205
    in
wenzelm@42007
   206
      session_info :=
wenzelm@51399
   207
        SOME (make_session_info (name, chapter, info_path, info, doc,
wenzelm@59446
   208
          doc_output, doc_files, graph_file, documents, verbose, readme));
wenzelm@59448
   209
      Synchronized.change browser_info (K empty_browser_info);
wenzelm@59448
   210
      add_html_index (0, HTML.begin_session_index name (Url.File session_graph_path) docs)
wenzelm@42008
   211
    end;
wenzelm@7727
   212
wenzelm@7727
   213
wenzelm@28496
   214
(* isabelle tool wrappers *)
wenzelm@17082
   215
wenzelm@48805
   216
fun isabelle_document {verbose, purge} format name tags dir =
wenzelm@17082
   217
  let
wenzelm@48805
   218
    val s = "\"$ISABELLE_TOOL\" document" ^ (if purge then " -c" else "") ^ " -o '" ^ format ^ "' \
wenzelm@48805
   219
      \-n '" ^ name ^ "' -t '" ^ tags ^ "' " ^ File.shell_path dir ^ " 2>&1";
wenzelm@48805
   220
    val doc_path = Path.appends [dir, Path.parent, Path.basic name |> Path.ext format];
wenzelm@33682
   221
    val _ = if verbose then writeln s else ();
wenzelm@43850
   222
    val (out, rc) = Isabelle_System.bash_output s;
wenzelm@33682
   223
    val _ =
wenzelm@33682
   224
      if not (File.exists doc_path) orelse rc <> 0 then
wenzelm@33682
   225
        cat_error out ("Failed to build document " ^ quote (show_path doc_path))
wenzelm@33682
   226
      else if verbose then writeln out
wenzelm@33682
   227
      else ();
wenzelm@33682
   228
  in doc_path end;
wenzelm@17082
   229
wenzelm@17082
   230
wenzelm@11856
   231
(* finish session -- output all generated text *)
wenzelm@11856
   232
wenzelm@59058
   233
fun sorted_index index = map snd (sort (int_ord o apply2 fst) (rev index));
wenzelm@24150
   234
fun index_buffer index = Buffer.add (implode (sorted_index index)) Buffer.empty;
wenzelm@24150
   235
wenzelm@14922
   236
fun write_tex src name path =
wenzelm@28027
   237
  File.write_buffer (Path.append path (tex_path name)) src;
wenzelm@14922
   238
wenzelm@14922
   239
fun write_tex_index tex_index path =
wenzelm@24150
   240
  write_tex (index_buffer tex_index |> Buffer.add Latex.tex_trailer) doc_indexN path;
wenzelm@14922
   241
wenzelm@42008
   242
fun finish () =
wenzelm@59446
   243
  with_session_info () (fn {name, chapter, info, info_path, doc_format,
wenzelm@59445
   244
    doc_output, doc_files, graph_file, documents, verbose, readme, ...} =>
wenzelm@7727
   245
  let
wenzelm@59448
   246
    val {theories, tex_index, html_index} = Synchronized.value browser_info;
wenzelm@11856
   247
    val thys = Symtab.dest theories;
wenzelm@51399
   248
wenzelm@51399
   249
    val chapter_prefix = Path.append info_path (Path.basic chapter);
wenzelm@51399
   250
    val session_prefix = Path.append chapter_prefix (Path.basic name);
wenzelm@7727
   251
wenzelm@54456
   252
    fun finish_html (a, {html_source, ...}: theory_info) =
wenzelm@54456
   253
      File.write (Path.append session_prefix (html_path a)) html_source;
wenzelm@11856
   254
wenzelm@42007
   255
    val _ =
wenzelm@42007
   256
      if info then
wenzelm@51399
   257
       (Isabelle_System.mkdirs session_prefix;
wenzelm@51399
   258
        File.write_buffer (Path.append session_prefix index_path)
wenzelm@51399
   259
          (index_buffer html_index |> Buffer.add HTML.end_document);
wenzelm@59448
   260
        Isabelle_System.copy_file graph_file (Path.append session_prefix session_graph_path);
wenzelm@56533
   261
        (case readme of NONE => () | SOME path => Isabelle_System.copy_file path session_prefix);
wenzelm@56533
   262
        Isabelle_System.copy_file (Path.explode "~~/etc/isabelle.css") session_prefix;
wenzelm@42007
   263
        List.app finish_html thys;
wenzelm@54455
   264
        if verbose
wenzelm@54455
   265
        then Output.physical_stderr ("Browser info at " ^ show_path session_prefix ^ "\n")
wenzelm@42007
   266
        else ())
wenzelm@42007
   267
      else ();
wenzelm@42007
   268
wenzelm@56533
   269
    fun document_job doc_prefix backdrop (doc_name, tags) =
wenzelm@48935
   270
      let
wenzelm@56533
   271
        val doc_dir = Path.append doc_prefix (Path.basic doc_name);
wenzelm@56531
   272
        val _ = Isabelle_System.mkdirs doc_dir;
wenzelm@56531
   273
        val _ =
wenzelm@56531
   274
          Isabelle_System.isabelle_tool "latex"
wenzelm@56531
   275
            ("-o sty " ^ File.shell_path (Path.append doc_dir (Path.basic "root.tex")));
wenzelm@57885
   276
        val _ = List.app (fn file => Isabelle_System.copy_file_base file doc_dir) doc_files;
wenzelm@59448
   277
        val _ = Isabelle_System.copy_file graph_file (Path.append doc_dir session_graph_path);
wenzelm@56531
   278
        val _ = write_tex_index tex_index doc_dir;
wenzelm@56531
   279
        val _ =
wenzelm@56531
   280
          List.app (fn (a, {tex_source, ...}) =>
wenzelm@56531
   281
            write_tex (Buffer.add tex_source Buffer.empty) a doc_dir) thys;
wenzelm@48935
   282
      in
wenzelm@48935
   283
        fn () =>
wenzelm@56533
   284
          (isabelle_document {verbose = true, purge = backdrop} doc_format doc_name tags doc_dir,
wenzelm@56531
   285
            fn doc =>
wenzelm@56531
   286
              if verbose orelse not backdrop then
wenzelm@56531
   287
                Output.physical_stderr ("Document at " ^ show_path doc ^ "\n")
wenzelm@56531
   288
              else ())
wenzelm@48935
   289
      end;
wenzelm@48935
   290
wenzelm@48935
   291
    val jobs =
wenzelm@48935
   292
      (if info orelse is_none doc_output then
wenzelm@51399
   293
        map (document_job session_prefix true) documents
wenzelm@48935
   294
       else []) @
wenzelm@48935
   295
      (case doc_output of
wenzelm@48935
   296
        NONE => []
wenzelm@48935
   297
      | SOME path => map (document_job path false) documents);
wenzelm@48935
   298
wenzelm@48935
   299
    val _ = jobs |> Par_List.map (fn job => job ()) |> List.app (op |>);
wenzelm@7727
   300
  in
wenzelm@59173
   301
    Synchronized.change browser_info (K empty_browser_info);
skalberg@15531
   302
    session_info := NONE
wenzelm@42008
   303
  end);
wenzelm@7727
   304
wenzelm@7727
   305
wenzelm@7727
   306
(* theory elements *)
wenzelm@7727
   307
wenzelm@9136
   308
fun theory_output name s =
wenzelm@54458
   309
  with_session_info () (fn _ =>
wenzelm@58870
   310
    change_theory_info name (fn (_, html_source) => (Latex.isabelle_theory name s, html_source)));
wenzelm@7727
   311
wenzelm@59448
   312
fun theory_link (curr_chapter, curr_session) thy =
wenzelm@59448
   313
  let
wenzelm@59448
   314
    val {chapter, name = session} = Browser_Info.get thy;
wenzelm@59448
   315
    val link = html_path (Context.theory_name thy);
wenzelm@59448
   316
  in
wenzelm@59448
   317
    if curr_session = session then SOME link
wenzelm@59448
   318
    else if curr_chapter = chapter then
wenzelm@59448
   319
      SOME (Path.appends [Path.parent, Path.basic session, link])
wenzelm@59448
   320
    else if chapter = Context.PureN then NONE
wenzelm@59448
   321
    else SOME (Path.appends [Path.parent, Path.parent, Path.basic chapter, Path.basic session, link])
wenzelm@59448
   322
  end;
wenzelm@59448
   323
wenzelm@54456
   324
fun begin_theory update_time mk_text thy =
wenzelm@54456
   325
  with_session_info thy (fn {name = session_name, chapter, ...} =>
wenzelm@54456
   326
    let
wenzelm@54456
   327
      val name = Context.theory_name thy;
wenzelm@54456
   328
      val parents = Theory.parents_of thy;
wenzelm@54456
   329
wenzelm@54456
   330
      val parent_specs = parents |> map (fn parent =>
wenzelm@54456
   331
        (Option.map Url.File (theory_link (chapter, session_name) parent),
wenzelm@54456
   332
          (Context.theory_name parent)));
wenzelm@54456
   333
      val html_source = HTML.theory name parent_specs (mk_text ());
wenzelm@54456
   334
    in
wenzelm@54456
   335
      init_theory_info name (make_theory_info ("", html_source));
wenzelm@54456
   336
      add_html_index (update_time, HTML.theory_entry (Url.File (html_path name), name));
wenzelm@54456
   337
      add_tex_index (update_time, Latex.theory_entry name);
wenzelm@54456
   338
      Browser_Info.put {chapter = chapter, name = session_name} thy
wenzelm@54456
   339
    end);
wenzelm@7727
   340
wenzelm@7727
   341
wenzelm@7727
   342
wenzelm@42127
   343
(** draft document output **)
wenzelm@14922
   344
wenzelm@52549
   345
fun display_drafts src_paths = Isabelle_System.with_tmp_dir "drafts" (fn dir =>
wenzelm@14922
   346
  let
wenzelm@24150
   347
    fun prep_draft path i =
wenzelm@14935
   348
      let
wenzelm@14935
   349
        val base = Path.base path;
wenzelm@14972
   350
        val name =
wenzelm@24829
   351
          (case Path.implode (#1 (Path.split_ext base)) of
wenzelm@44986
   352
            "" => "DUMMY"
wenzelm@44986
   353
          | s => s)  ^ serial_string ();
wenzelm@14935
   354
      in
wenzelm@14935
   355
        if File.exists path then
wenzelm@24150
   356
          (((name, base, File.read path), (i, Latex.theory_entry name)), i + 1)
wenzelm@41944
   357
        else error ("Bad file: " ^ Path.print path)
wenzelm@14935
   358
      end;
wenzelm@24150
   359
    val (srcs, tex_index) = split_list (fst (fold_map prep_draft src_paths 0));
wenzelm@14935
   360
wenzelm@42127
   361
    val doc_path = Path.append dir document_path;
wenzelm@40743
   362
    val _ = Isabelle_System.mkdirs doc_path;
wenzelm@14922
   363
    val root_path = Path.append doc_path (Path.basic "root.tex");
wenzelm@56533
   364
    val _ = Isabelle_System.copy_file (Path.explode "~~/lib/texinputs/draft.tex") root_path;
wenzelm@40743
   365
    val _ = Isabelle_System.isabelle_tool "latex" ("-o sty " ^ File.shell_path root_path);
wenzelm@40743
   366
    val _ = Isabelle_System.isabelle_tool "latex" ("-o syms " ^ File.shell_path root_path);
wenzelm@14922
   367
wenzelm@14922
   368
    fun known name =
wenzelm@14922
   369
      let val ss = split_lines (File.read (Path.append doc_path (Path.basic name)))
wenzelm@20664
   370
      in member (op =) ss end;
wenzelm@14922
   371
    val known_syms = known "syms.lst";
wenzelm@14922
   372
    val known_ctrls = known "ctrls.lst";
wenzelm@14922
   373
skalberg@15570
   374
    val _ = srcs |> List.app (fn (name, base, txt) =>
wenzelm@14935
   375
      Symbol.explode txt
wenzelm@21858
   376
      |> Latex.symbol_source (known_syms, known_ctrls) (Path.implode base)
wenzelm@14935
   377
      |> File.write (Path.append doc_path (tex_path name)));
wenzelm@14922
   378
    val _ = write_tex_index tex_index doc_path;
wenzelm@14922
   379
wenzelm@48805
   380
    val result =
wenzelm@52743
   381
      isabelle_document {verbose = false, purge = true} "pdf" documentN "" doc_path;
wenzelm@54683
   382
wenzelm@54683
   383
    val target_dir = Path.explode "$ISABELLE_HOME_USER/tmp";
wenzelm@54683
   384
    val target = Path.explode "$ISABELLE_HOME_USER/tmp/drafts.pdf"
wenzelm@54683
   385
    val _ = Isabelle_System.mkdirs target_dir;
wenzelm@56533
   386
    val _ = Isabelle_System.copy_file result target;
wenzelm@52549
   387
  in
wenzelm@54683
   388
    Isabelle_System.isabelle_tool "display" (File.shell_path target ^ " &")
wenzelm@52549
   389
  end);
wenzelm@14922
   390
wenzelm@7685
   391
end;