src/Tools/Code/code_runtime.ML
changeset 46947 b8c7eb0c2f89
parent 46737 09ab89658a5d
child 46949 94aa7b81bcf6
equal deleted inserted replaced
46946:acc8ebf980ca 46947:b8c7eb0c2f89
   347 val datatypesK = "datatypes";
   347 val datatypesK = "datatypes";
   348 val functionsK = "functions";
   348 val functionsK = "functions";
   349 val fileK = "file";
   349 val fileK = "file";
   350 val andK = "and"
   350 val andK = "and"
   351 
   351 
   352 val _ = List.app Keyword.keyword [datatypesK, functionsK];
       
   353 
       
   354 val parse_datatype =
   352 val parse_datatype =
   355   Parse.name --| Parse.$$$ "=" --
   353   Parse.name --| Parse.$$$ "=" --
   356     (((Parse.sym_ident || Parse.string) >> (fn "_" => NONE | _ => Scan.fail ()))
   354     (((Parse.sym_ident || Parse.string) >> (fn "_" => NONE | _ => Scan.fail ()))
   357     || ((Parse.term ::: (Scan.repeat (Parse.$$$ "|" |-- Parse.term))) >> SOME));
   355     || ((Parse.term ::: (Scan.repeat (Parse.$$$ "|" |-- Parse.term))) >> SOME));
   358 
   356