[m-dev.] diff: fix quoting bug: quote '#'

[Fergus Henderson]

Estimated hours taken: 0.25

library/term_io.m:
	In term_io__quote_atom, ensure that atoms starting with '#' are
	quoted, because Mercury uses '#' for source line number indicators.

Workspace: /home/mercury0/fjh/mercury-other
Index: library/term_io.m
===================================================================
RCS file: /home/mercury1/repository/mercury/library/term_io.m,v
retrieving revision 1.57
diff -u -r1.57 term_io.m
--- term_io.m	1998/11/20 04:10:35	1.57
+++ term_io.m	1999/06/09 14:14:49
@@ -444,6 +444,12 @@
 				\+ lexer__graphic_token_char(Char)) },
 			{ Chars \= [] },
 			%
+			% We need to quote tokens starting with '#',
+			% because Mercury uses '#' to start source line
+			% number indicators.
+			% 
+			{ Chars \= ['#' | _] },
+			%
 			% If the token could be the last token in a term,
 			% and the term could be followed with ".\n",
 			% then we need to quote the token, otherwise

-- 
Fergus Henderson <fjh at cs.mu.oz.au>  |  "I have always known that the pursuit
WWW: <http://www.cs.mu.oz.au/~fjh>  |  of excellence is a lethal habit"
PGP: finger fjh at 128.250.37.3        |     -- the last words of T. S. Garp.
--------------------------------------------------------------------------
mercury-developers mailing list
Post messages to:       mercury-developers at cs.mu.oz.au
Administrative Queries: owner-mercury-developers at cs.mu.oz.au
Subscriptions:          mercury-developers-request at cs.mu.oz.au
--------------------------------------------------------------------------