1.1 --- a/test/Pure/Isar/Test_Parsers.thy	Tue Jul 28 16:17:42 2020 +0200
     1.2 +++ b/test/Pure/Isar/Test_Parsers.thy	Fri Jul 31 12:21:34 2020 +0200
     1.3 @@ -187,6 +187,49 @@
     1.4  ML \<open>(*from Pure/Isar/args.ML, fun attribs*)
     1.5  Parse.$$$ "[" |-- Parse.list1 Parse.name --| Parse.$$$ "]";
     1.6  (*fn : Token.T list -> bstring list * Token.T list*)
     1.7 +\<close> ML \<open>
     1.8 +\<close> ML \<open> (* example close to lists see Cookbook p.144 \<section>6.2 *)
     1.9 +let
    1.10 +  val input = filtered_input "in , in , in"
    1.11 +  val p = Parse.enum "," (Parse.$$$ "in")
    1.12 +in
    1.13 +  Scan.finite Token.stopper p input
    1.14 +end
    1.15 +(* = (["in", "in", "in"], []) *)
    1.16 +\<close> ML \<open>
    1.17 +let
    1.18 +  val input = filtered_input "aaa , bbb , ccc"
    1.19 +  val p = Parse.enum "," Parse.name
    1.20 +in
    1.21 +  Scan.finite Token.stopper p input
    1.22 +end
    1.23 +(* = (["aaa", "bbb", "ccc"], []) *)
    1.24 +\<close> ML \<open>
    1.25 +let
    1.26 +  val input = filtered_input "\"aaa\" , \"bbb\" , \"ccc\""
    1.27 +  val p = Parse.enum "," Parse.string
    1.28 +in
    1.29 +  Scan.finite Token.stopper p input
    1.30 +end
    1.31 +(* = (["aaa", "bbb", "ccc"], []) *)
    1.32 +\<close> ML \<open>
    1.33 +let
    1.34 +  val input = filtered_input "\"aaa\" , \"bbb\" , \"ccc\""
    1.35 +  val p = Parse.list1 Parse.string
    1.36 +in
    1.37 +  Scan.finite Token.stopper p input
    1.38 +end
    1.39 +(* = (["aaa", "bbb", "ccc"], []) *)
    1.40 +\<close> ML \<open>
    1.41 +let
    1.42 +  val input = filtered_input "[\"aaa\" , \"bbb\" , \"ccc\"]"
    1.43 +  val p = Parse.$$$ "[" |-- Parse.list1 Parse.string --| Parse.$$$ "]"
    1.44 +in
    1.45 +  Scan.finite Token.stopper p input
    1.46 +end
    1.47 +(* = (["aaa", "bbb", "ccc"], []) *)
    1.48 +
    1.49 +
    1.50  
    1.51  \<close> ML \<open>
    1.52  parse (Parse.$$$ "[" |-- Parse.list Parse.name --| Parse.$$$ "]")