diff -r aa14f630d8ef -r 564012e31db1 src/Pure/PIDE/session.ML
--- 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);