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/Pure/Syntax/syntax_ext.ML
changeset 63933 e149e3e320a3
parent 63806 c54a53ef1873
child 64677 8dc24130e8fe 
--- a/src/Pure/Syntax/syntax_ext.ML	Wed Sep 21 20:33:44 2016 +0200
+++ b/src/Pure/Syntax/syntax_ext.ML	Wed Sep 21 22:43:06 2016 +0200
@@ -251,9 +251,10 @@
 
 val is_meta = member (op =) ["(", ")", "/", "_", "\<index>", Symbol.open_, Symbol.close];
 
-val scan_delim_char =
-  $$ "'" |-- scan_one ((not o Symbol.is_blank) andf Symbol.not_eof) ||
-  scan_one ((not o is_meta) andf (not o Symbol.is_blank) andf Symbol.not_eof);
+val scan_delim =
+  scan_one Symbol.is_control ::: Symbol_Pos.scan_cartouche "Mixfix error: " ||
+  $$ "'" |-- scan_one ((not o Symbol.is_blank) andf Symbol.not_eof) >> single ||
+  scan_one ((not o is_meta) andf (not o Symbol.is_blank) andf Symbol.not_eof) >> single;
 
 val scan_sym =
   $$ "_" >> K (Argument ("", 0)) ||
@@ -265,7 +266,7 @@
   $$ "/" -- $$ "/" >> K (Brk ~1) ||
   $$ "/" |-- scan_many Symbol.is_space >> (Brk o length) ||
   scan_many1 Symbol.is_space >> (Space o Symbol_Pos.content) ||
-  Scan.repeat1 scan_delim_char >> (Delim o Symbol_Pos.content);
+  Scan.repeat1 scan_delim >> (Delim o Symbol_Pos.content o flat);
 
 val scan_symb =
   Scan.trace scan_sym >> (fn (syms, trace) => SOME (syms, #1 (Symbol_Pos.range trace))) ||
isabelle