src/Pure/Thy/sessions.ML

 val document_files =
   Parse.$$$ "document_files" |--
     Parse.!!! (Scan.optional in_path ("document", Position.none)
       -- Scan.repeat1 (Parse.position Parse.path));
 
+val prune =
+  Scan.optional (Parse.$$$ "[" |-- Parse.!!! (Parse.nat --| Parse.$$$ "]")) 0;
+
 val export_files =
   Parse.$$$ "export_files" |--
-    Parse.!!! (Scan.optional in_path ("export", Position.none) -- Scan.repeat1 Parse.embedded);
+    Parse.!!!
+      (Scan.optional in_path ("export", Position.none) -- prune -- Scan.repeat1 Parse.embedded);
 
 in
 
 val command_parser =
   Parse.session_name --

               val dir = Resources.check_dir ctxt session_dir doc_dir;
               val _ = List.app (ignore o Resources.check_file ctxt dir) doc_files;
             in () end);
 
         val _ =
-          export_files |> List.app (fn (export_dir, _) =>
+          export_files |> List.app (fn ((export_dir, _), _) =>
             ignore (Resources.check_path ctxt session_dir export_dir));
       in () end));
 
 end;