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/Tools/WWW_Find/unicode_symbols.ML
changeset 48992 0518bf89c777
parent 43947 9b00f09f7721
child 50135 d5132bba6a83 
--- a/src/Tools/WWW_Find/unicode_symbols.ML	Wed Aug 29 11:31:07 2012 +0200
+++ b/src/Tools/WWW_Find/unicode_symbols.ML	Wed Aug 29 11:48:45 2012 +0200
@@ -109,7 +109,7 @@
       (toks, []) => toks
     | (_, ss) =>
         error ("Lexical error at: " ^ Symbol_Pos.content ss ^
-          Position.str_of (#1 (Symbol_Pos.range ss))))
+          Position.here (#1 (Symbol_Pos.range ss))))
   end;
 
 val stopper =
@@ -152,8 +152,8 @@
         Symtab.update_new (abbr, uni) fromabbr,
         Inttab.update (uni, sym) tosym,
         Inttab.update (uni, abbr) toabbr))
-  handle Symtab.DUP sym => error ("Duplicate at" ^ Position.str_of pos)
-       | Inttab.DUP sym => error ("Duplicate code at" ^ Position.str_of pos);
+  handle Symtab.DUP sym => error ("Duplicate at" ^ Position.here pos)
+       | Inttab.DUP sym => error ("Duplicate code at" ^ Position.here pos);
 
 in
isabelle