annotate src/errormsg.sml @ 665:910bf013da4a

Mention src/coq in CHANGELOG
author Adam Chlipala <adamc@hcoop.net>
date Thu, 12 Mar 2009 12:37:02 -0400
parents 8f8771f32909
children 9b54fbe1efdb
rev   line source
adamc@0 1 (* Copyright (c) 2008, Adam Chlipala
adamc@0 2 * All rights reserved.
adamc@0 3 *
adamc@0 4 * Redistribution and use in source and binary forms, with or without
adamc@0 5 * modification, are permitted provided that the following conditions are met:
adamc@0 6 *
adamc@0 7 * - Redistributions of source code must retain the above copyright notice,
adamc@0 8 * this list of conditions and the following disclaimer.
adamc@0 9 * - Redistributions in binary form must reproduce the above copyright notice,
adamc@0 10 * this list of conditions and the following disclaimer in the documentation
adamc@0 11 * and/or other materials provided with the distribution.
adamc@0 12 * - The names of contributors may not be used to endorse or promote products
adamc@0 13 * derived from this software without specific prior written permission.
adamc@0 14 *
adamc@0 15 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
adamc@0 16 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
adamc@0 17 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
adamc@0 18 * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
adamc@0 19 * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
adamc@0 20 * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
adamc@0 21 * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
adamc@0 22 * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
adamc@0 23 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
adamc@0 24 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
adamc@0 25 * POSSIBILITY OF SUCH DAMAGE.
adamc@0 26 *)
adamc@0 27
adamc@0 28 structure ErrorMsg :> ERROR_MSG = struct
adamc@0 29
adamc@0 30 type pos = {line : int,
adamc@0 31 char : int}
adamc@0 32
adamc@0 33 type span = {file : string,
adamc@0 34 first : pos,
adamc@0 35 last : pos}
adamc@0 36
adamc@0 37 type 'a located = 'a * span
adamc@0 38
adamc@1 39
adamc@1 40 fun posToString {line, char} =
adamc@1 41 String.concat [Int.toString line, ":", Int.toString char]
adamc@1 42
adamc@1 43 fun spanToString {file, first, last} =
adamc@1 44 String.concat [file, ":", posToString first, "-", posToString last]
adamc@1 45
adamc@3 46 val dummyPos = {line = 0,
adamc@3 47 char = 0}
adamc@3 48 val dummySpan = {file = "",
adamc@3 49 first = dummyPos,
adamc@3 50 last = dummyPos}
adamc@3 51
adamc@1 52
adamc@1 53 val file = ref ""
adamc@1 54 val numLines = ref 1
adamc@1 55 val lines : int list ref = ref []
adamc@1 56
adamc@1 57 fun resetPositioning fname = (file := fname;
adamc@1 58 numLines := 1;
adamc@1 59 lines := [])
adamc@1 60
adamc@1 61 fun newline pos = (numLines := !numLines + 1;
adamc@1 62 lines := pos :: !lines)
adamc@1 63
adamc@1 64 fun lastLineStart () =
adamc@1 65 case !lines of
adamc@1 66 [] => 0
adamc@1 67 | n :: _ => n+1
adamc@1 68
adamc@1 69 fun posOf n =
adamc@1 70 let
adamc@1 71 fun search lineNum lines =
adamc@1 72 case lines of
adamc@1 73 [] => {line = 1,
adamc@1 74 char = n}
adamc@1 75 | bound :: rest =>
adamc@1 76 if n > bound then
adamc@1 77 {line = lineNum,
adamc@1 78 char = n - bound - 1}
adamc@1 79 else
adamc@1 80 search (lineNum - 1) rest
adamc@1 81 in
adamc@1 82 search (!numLines) (!lines)
adamc@1 83 end
adamc@1 84
adamc@1 85 fun spanOf (pos1, pos2) = {file = !file,
adamc@1 86 first = posOf pos1,
adamc@1 87 last = posOf pos2}
adamc@1 88
adamc@1 89
adamc@1 90 val errors = ref false
adamc@1 91
adamc@1 92 fun resetErrors () = errors := false
adamc@1 93 fun anyErrors () = !errors
adamc@1 94 fun error s = (TextIO.output (TextIO.stdErr, s);
adamc@1 95 TextIO.output1 (TextIO.stdErr, #"\n");
adamc@1 96 errors := true)
adamc@1 97 fun errorAt span s = (TextIO.output (TextIO.stdErr, spanToString span);
adamc@591 98 TextIO.output (TextIO.stdErr, ": ");
adamc@1 99 error s)
adamc@1 100 fun errorAt' span s = errorAt (spanOf span) s
adamc@1 101
adamc@0 102 end