--- a/src/Pure/PIDE/session.ML Sat Sep 26 11:43:25 2020 +0200
+++ b/src/Pure/PIDE/session.ML Sat Sep 26 14:29:46 2020 +0200
@@ -46,13 +46,17 @@
(* init *)
+val document =
+ fn "" => false | "false" => false | "pdf" => true
+ | doc => error ("Bad document specification " ^ quote doc);
+
fun init symbols info info_path doc doc_output doc_variants doc_files graph_file
parent (chapter, name) verbose =
(Synchronized.change session (fn ({name = parent_name, ...}, parent_finished) =>
if parent_name <> parent orelse not parent_finished then
error ("Unfinished parent session " ^ quote parent ^ " for " ^ quote name)
else ({chapter = chapter, name = name}, false));
- Present.init symbols info info_path (if doc = "false" then "" else doc)
+ Present.init symbols info info_path (document doc)
doc_output doc_variants doc_files graph_file (chapter, name) verbose);