Mercurial > urweb

comparison src/compiler.sml @ 1151:de48dc2c9ee8

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Allow .urp files without initial blank lines
author Adam Chlipala <adamc@hcoop.net>
date Sat, 06 Feb 2010 15:34:41 -0500
parents 7fdea74b1dd9
children 76f607cefdb1
comparison
equal deleted inserted replaced
1150:151837581b5e 1151:de48dc2c9ee8
280 val bigLibs = ref [] 280 val bigLibs = ref []
281 281
282 fun pu filename = 282 fun pu filename =
283 let 283 let
284 val dir = OS.Path.dir filename 284 val dir = OS.Path.dir filename
285 val inf = TextIO.openIn (OS.Path.joinBaseExt {base = filename, ext = SOME "urp"}) 285 fun opener () = TextIO.openIn (OS.Path.joinBaseExt {base = filename, ext = SOME "urp"})
286
287 val inf = opener ()
288
289 fun hasAnyLine () =
290 case TextIO.inputLine inf of
291 NONE => false
292 | SOME "\n" => false
293 | _ => true
294
295 fun hasBlankLine () =
296 case TextIO.inputLine inf of
297 NONE => false
298 | SOME "\n" => hasAnyLine ()
299 | _ => hasBlankLine ()
300
301 val hasBlankLine = hasBlankLine ()
302
303 val inf = (TextIO.closeIn inf; opener ())
286 304
287 fun pathify fname = 305 fun pathify fname =
288 if size fname > 0 andalso String.sub (fname, 0) = #"$" then 306 if size fname > 0 andalso String.sub (fname, 0) = #"$" then
289 let 307 let
290 val fname' = Substring.extract (fname, 1, NONE) 308 val fname' = Substring.extract (fname, 1, NONE)
589 | _ => ErrorMsg.error "path argument not of the form name=value'") 607 | _ => ErrorMsg.error "path argument not of the form name=value'")
590 | _ => ErrorMsg.error ("Unrecognized command '" ^ cmd ^ "'"); 608 | _ => ErrorMsg.error ("Unrecognized command '" ^ cmd ^ "'");
591 read () 609 read ()
592 end 610 end
593 611
594 val job = read () 612 val job = if hasBlankLine then
613 read ()
614 else
615 finish (readSources [])
595 in 616 in
596 TextIO.closeIn inf; 617 TextIO.closeIn inf;
597 Settings.setUrlPrefix (#prefix job); 618 Settings.setUrlPrefix (#prefix job);
598 Settings.setTimeout (#timeout job); 619 Settings.setTimeout (#timeout job);
599 Settings.setHeaders (#headers job); 620 Settings.setHeaders (#headers job);