Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/Thy/sessions.ML
changeset 76614 ac08b6e3b9e3
parent 76005 a9bbf075f431 
--- a/src/Pure/Thy/sessions.ML	Sat Dec 10 15:57:21 2022 +0100
+++ b/src/Pure/Thy/sessions.ML	Sat Dec 10 20:31:47 2022 +0100
@@ -31,22 +31,19 @@
 val theories =
   Parse.$$$ "theories" |-- Parse.!!! (Scan.optional Parse.options [] -- Scan.repeat1 theory_entry);
 
-val in_path =
-  Parse.$$$ "(" |-- Parse.!!! (Parse.$$$ "in" |-- Parse.path_input --| Parse.$$$ ")");
-
 val document_theories =
   Parse.$$$ "document_theories" |-- Scan.repeat1 (Parse.input Parse.theory_name);
 
 val document_files =
   Parse.$$$ "document_files" |--
-    Parse.!!! (Scan.optional in_path (Input.string "document") -- Scan.repeat1 Parse.path_input);
+    Parse.!!! (Parse.in_path_parens "document" -- Scan.repeat1 Parse.path_input);
 
 val prune =
   Scan.optional (Parse.$$$ "[" |-- Parse.!!! (Parse.nat --| Parse.$$$ "]")) 0;
 
 val export_files =
   Parse.$$$ "export_files" |--
-    Parse.!!! (Scan.optional in_path (Input.string "export") -- prune -- Scan.repeat1 Parse.embedded);
+    Parse.!!! (Parse.in_path_parens "export" -- prune -- Scan.repeat1 Parse.embedded);
 
 val export_classpath =
   Parse.$$$ "export_classpath" |-- Scan.repeat Parse.embedded;
@@ -68,8 +65,7 @@
       in () end));
 
 val session_parser =
-  Parse.session_name -- groups --
-  Scan.optional (Parse.$$$ "in" |-- Parse.!!! Parse.path_input) (Input.string ".") --
+  Parse.session_name -- groups -- Parse.in_path "." --
   (Parse.$$$ "=" |--
     Parse.!!! (Scan.option (Parse.session_name --| Parse.!!! (Parse.$$$ "+")) -- description --
       Scan.optional (Parse.$$$ "options" |-- Parse.!!! Parse.options) [] --
isabelle