src/Pure/Thy/bibtex.ML
changeset 72194 eef421b724c0
parent 71881 71de0a253842
child 72613 d01ea9e3bd2d
equal deleted inserted replaced
72193:742d94015918 72194:eef421b724c0
    18 (* check database *)
    18 (* check database *)
    19 
    19 
    20 type message = string * Position.T;
    20 type message = string * Position.T;
    21 
    21 
    22 fun check_database pos0 database =
    22 fun check_database pos0 database =
    23   \<^scala>\<open>check_bibtex_database\<close> database
    23   \<^scala>\<open>bibtex_check_database\<close> database
    24   |> YXML.parse_body
    24   |> YXML.parse_body
    25   |> let open XML.Decode in pair (list (pair string properties)) (list (pair string properties)) end
    25   |> let open XML.Decode in pair (list (pair string properties)) (list (pair string properties)) end
    26   |> (apply2 o map o apsnd) (fn pos => Position.of_properties (pos @ Position.get_props pos0));
    26   |> (apply2 o map o apsnd) (fn pos => Position.of_properties (pos @ Position.get_props pos0));
    27 
    27 
    28 fun check_database_output pos0 database =
    28 fun check_database_output pos0 database =