# HG changeset patch
# User Adam Chlipala <adamc@hcoop.net>
# Date 1214147050 14400
# Node ID 5c97b7cd912b63277ed75dca84877da89d630c5a
# Parent  a6e185c7c4283121251de7148ddf5f82b3dca7b3
Parsing signature files

diff -r a6e185c7c428 -r 5c97b7cd912b src/compiler.sig
--- a/src/compiler.sig	Sun Jun 22 10:53:11 2008 -0400
+++ b/src/compiler.sig	Sun Jun 22 11:04:10 2008 -0400
@@ -31,6 +31,9 @@
 
     val compile : string -> unit
 
+    val parseLig : string -> Source.sgn_item list option
+    val testLig : string -> unit
+
     val parse : string -> Source.file option
     val elaborate : ElabEnv.env -> string -> (Elab.file * ElabEnv.env) option
     val explify : ElabEnv.env -> string -> Expl.file option
diff -r a6e185c7c428 -r 5c97b7cd912b src/compiler.sml
--- a/src/compiler.sml	Sun Jun 22 10:53:11 2008 -0400
+++ b/src/compiler.sml	Sun Jun 22 11:04:10 2008 -0400
@@ -35,6 +35,46 @@
                          structure Lex = Lex
                          structure LrParser = LrParser)
 
+fun parseLig filename =
+    let
+        val fname = OS.FileSys.tmpName ()
+        val outf = TextIO.openOut fname
+        val () = TextIO.output (outf, "sig\n")
+        val inf = TextIO.openIn filename
+        fun loop () =
+            case TextIO.inputLine inf of
+                NONE => ()
+              | SOME line => (TextIO.output (outf, line);
+                              loop ())
+        val () = loop ()
+        val () = TextIO.closeIn inf
+        val () = TextIO.closeOut outf
+
+        val () = (ErrorMsg.resetErrors ();
+                  ErrorMsg.resetPositioning filename)
+	val file = TextIO.openIn fname
+	fun get _ = TextIO.input file
+	fun parseerror (s, p1, p2) = ErrorMsg.errorAt' (p1, p2) s
+	val lexer = LrParser.Stream.streamify (Lex.makeLexer get)
+	val (absyn, _) = LacwebP.parse (30, lexer, parseerror, ())
+    in
+        TextIO.closeIn file;
+        if ErrorMsg.anyErrors () then
+            NONE
+        else
+            case absyn of
+                [(Source.DSgn ("?", (Source.SgnConst sgis, _)), _)] => SOME sgis
+              | _ => NONE
+    end
+    handle LrParser.ParseError => NONE
+
+fun testLig fname =
+    case parseLig fname of
+        NONE => ()
+      | SOME sgis =>
+        app (fn sgi => (Print.print (SourcePrint.p_sgn_item sgi);
+                        print "\n")) sgis
+
 (* The main parsing routine *)
 fun parse filename =
     let
@@ -50,7 +90,11 @@
         if ErrorMsg.anyErrors () then
             NONE
         else
-            SOME absyn
+            case absyn of
+                [(Source.DSgn ("?", _), _)] =>
+                (ErrorMsg.error "File starts with 'sig'";
+                 NONE)
+              | _ => SOME absyn
     end
     handle LrParser.ParseError => NONE
 
diff -r a6e185c7c428 -r 5c97b7cd912b src/source_print.sig
--- a/src/source_print.sig	Sun Jun 22 10:53:11 2008 -0400
+++ b/src/source_print.sig	Sun Jun 22 11:04:10 2008 -0400
@@ -32,5 +32,6 @@
     val p_explicitness : Source.explicitness Print.printer
     val p_con : Source.con Print.printer
     val p_decl : Source.decl Print.printer
+    val p_sgn_item : Source.sgn_item Print.printer
     val p_file : Source.file Print.printer
 end
diff -r a6e185c7c428 -r 5c97b7cd912b tests/split.lac
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/tests/split.lac	Sun Jun 22 11:04:10 2008 -0400
@@ -0,0 +1,2 @@
+type t = int
+val x = 0
diff -r a6e185c7c428 -r 5c97b7cd912b tests/split.lig
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/tests/split.lig	Sun Jun 22 11:04:10 2008 -0400
@@ -0,0 +1,2 @@
+type t
+val x : t