equal
deleted
inserted
replaced
894 \ val f' = !f\n\ |
894 \ val f' = !f\n\ |
895 \ in (f := (fn x' => if x = x' then y else f' x'); y) end))\n\ |
895 \ in (f := (fn x' => if x = x' then y else f' x'); y) end))\n\ |
896 \ in (fn x => !f x) end;\n")]))]]; |
896 \ in (fn x => !f x) end;\n")]))]]; |
897 |
897 |
898 |
898 |
899 structure P = OuterParse and K = OuterSyntax.Keyword; |
899 structure P = OuterParse and K = OuterKeyword; |
900 |
900 |
901 fun strip_newlines s = implode (fst (take_suffix (equal "\n") |
901 fun strip_newlines s = implode (fst (take_suffix (equal "\n") |
902 (snd (take_prefix (equal "\n") (explode s))))) ^ "\n"; |
902 (snd (take_prefix (equal "\n") (explode s))))) ^ "\n"; |
903 |
903 |
904 val parse_attach = Scan.repeat (P.$$$ "attach" |-- |
904 val parse_attach = Scan.repeat (P.$$$ "attach" |-- |