Various enhancements to --wiki

src/main/java/jhilbert/JHilbertException.java

@@ -52,4 +52,19 @@ public JHilbertException(final String message, final Throwable cause) {
 		super(message, cause);
 	}
 
+	public boolean messageMatches(String expectedError) {
+		if (expectedError.equals(getMessage())) {
+			return true;
+		}
+		else if (getCause() instanceof JHilbertException) {
+			return ((JHilbertException) getCause()).messageMatches(expectedError);
+		}
+		else if (null != getCause()) {
+			return expectedError.equals(getCause().getMessage());
+		}
+		else {
+			return false;
+		}
+	}
+
 }

src/main/java/jhilbert/Main.java

@@ -40,6 +40,7 @@ See the commit logs ("git log") for a list of individual contributions.
 import jhilbert.scanners.ScannerFactory;
 import jhilbert.scanners.TokenFeed;
 import jhilbert.scanners.WikiInputStream;
+import jhilbert.scanners.impl.WikiStreamTokenFeed;
 
 import org.apache.log4j.BasicConfigurator;
 import org.apache.log4j.ConsoleAppender;
@@ -186,23 +187,22 @@ public static void main(String... args) throws Exception {
 	}
 
 	private static void processWikiFile(String inputFileName)
-	  throws IOException, ScannerException, CommandException {
+	  throws IOException, JHilbertException {
 		if (isInterface(inputFileName)) {
 			logger.info("Processing interface " + inputFileName);
 
-			final Module mainInterface = DataFactory.getInstance().createModule(inputFileName);
-			final TokenFeed tokenFeed = ScannerFactory
-				.getInstance().createTokenFeed(WikiInputStream.create(inputFileName));
-			CommandFactory.getInstance().processCommands(mainInterface, tokenFeed);
+			WikiInputStream wiki = WikiInputStream.create(inputFileName);
+			final Module mainInterface = DataFactory.getInstance().
+				createInterface(inputFileName);
+			process(wiki, mainInterface);
 			logger.info("File processed successfully");
 		}
 		else if (isProofModule(inputFileName)) {
 			logger.info("Processing proof module " + inputFileName);
 
-			final Module mainModule = DataFactory.getInstance().createModule("");
-			final TokenFeed tokenFeed = ScannerFactory
-				.getInstance().createTokenFeed(WikiInputStream.create(inputFileName));
-			CommandFactory.getInstance().processCommands(mainModule, tokenFeed);
+			WikiInputStream wiki = WikiInputStream.create(inputFileName);
+			final Module mainModule = DataFactory.getInstance().createProofModule();
+			process(wiki, mainModule);
 			logger.info("File processed successfully");
 		}
 		else {
@@ -211,6 +211,37 @@ else if (isProofModule(inputFileName)) {
 		}
 	}
 
+	static void process(WikiInputStream wiki, final Module module)
+			throws JHilbertException {
+		String expectedError;
+		if (wiki.expectedErrors().size() > 1) {
+			throw new JHilbertException("can only expect one error per file currently");
+		}
+		else if (wiki.expectedErrors().size() == 1) {
+			expectedError = wiki.expectedErrors().get(0);
+		}
+		else {
+			expectedError = null;
+		}
+
+		final WikiStreamTokenFeed tokenFeed = new WikiStreamTokenFeed(wiki);
+		try {
+			CommandFactory.getInstance().processCommands(module, tokenFeed);
+		}
+		catch (JHilbertException e) {
+			if (expectedError != null) {
+				if (!e.messageMatches(expectedError)
+						&& !tokenFeed.hasRejection(expectedError)) {
+					throw new JHilbertException("expected error:\n  " + expectedError +
+						"\nbut got:\n  " + e.getMessage());
+				}
+			}
+			else {
+				throw e;
+			}
+		}
+	}
+
 	public static boolean isProofModule(String fileName) {
 		return fileName.contains("Main/") ||
 		  fileName.contains("User module/");
@@ -224,7 +255,7 @@ public static boolean isInterface(String fileName) {
 	private static void processProofModule(String inputFileName)
 			throws ScannerException, FileNotFoundException, CommandException {
 		logger.info("Processing file " + inputFileName);
-		final Module mainModule = DataFactory.getInstance().createModule("");
+		final Module mainModule = DataFactory.getInstance().createProofModule();
 		final TokenFeed tokenFeed = ScannerFactory
 			.getInstance().createTokenFeed(new FileInputStream(inputFileName));
 		CommandFactory.getInstance().processCommands(mainModule, tokenFeed);

src/main/java/jhilbert/data/DataFactory.java

@@ -64,6 +64,17 @@ public final Module createModule(String name) {
 		}
 	}
 
+	public final Module createProofModule() {
+		return createModule("");
+	}
+
+	public final Module createInterface(String name) {
+		if (name == null || "".equals(name)) {
+			throw new IllegalArgumentException("must give a name to an interface");
+		}
+		return createModule(name);
+	}
+
 	/**
 	 * Creates a new {@link Module} with the specified name and revision
 	 * number.

src/main/java/jhilbert/data/impl/NamespaceImpl.java

@@ -118,7 +118,7 @@ public void registerObject(final Name o) throws DataException {
 		if (registry.containsKey(name)) {
 			logger.error("Name " + name + " already registered in this namespace");
 			logger.debug("Previously registered object: " + registry.get(name));
-			throw new DataException("Name already registered");
+			throw new DataException("Name " + name + " already registered");
 		}
 		registry.put(name, obj);
 		obj.setNamespace(this);

src/main/java/jhilbert/data/impl/StatementImpl.java

@@ -55,6 +55,7 @@ final class StatementImpl extends SymbolImpl implements Statement, Serializable
 	/**
 	 * Logger for this class.
 	 */
+	@SuppressWarnings("unused")
 	private static final Logger logger = Logger.getLogger(StatementImpl.class);
 
 	/**

src/main/java/jhilbert/scanners/WikiInputStream.java

@@ -29,39 +29,107 @@ See the commit logs ("git log") for a list of individual contributions.
 import java.io.FileInputStream;
 import java.io.IOException;
 import java.io.InputStream;
+import java.io.StringWriter;
+import java.io.Writer;
+import java.util.ArrayList;
+import java.util.List;
 import java.util.regex.Matcher;
 import java.util.regex.Pattern;
 
 public class WikiInputStream extends InputStream {
 
-	// This class contains only static methods
+	private InputStream delegate;
+	private Writer buffer;
+	private String contents;
+	private ArrayList<String> expectedErrors;
+
 	private WikiInputStream() {
+		this.buffer = new StringWriter();
+		expectedErrors = new ArrayList();
+	}
+
+	private void finishWriting() throws IOException {
+		buffer.flush();
+		contents = buffer.toString();
+		delegate = new ByteArrayInputStream(contents.getBytes("UTF-8"));
+		buffer = null;
+	}
+
+	private String getContents() {
+		return contents;
 	}
 
 	@Override
 	public int read() throws IOException {
-		throw new RuntimeException("This class contains only static methods");
+		return delegate.read();
+	}
+
+	@Override
+	public void close() throws IOException {
+		delegate.close();
+	}
+
+	@Override
+	public int read(byte[] arg0, int arg1, int arg2) throws IOException {
+		return delegate.read(arg0, arg1, arg2);
 	}
 
-	public static InputStream create(String inputFileName) throws IOException {
+	@Override
+	public int read(byte[] b) throws IOException {
+		return delegate.read(b);
+	}
+
+	public static WikiInputStream create(String inputFileName) throws IOException {
 		return create(new FileInputStream(inputFileName));
 	}
 
-	public static InputStream create(InputStream inputStream) throws IOException {
-		return new ByteArrayInputStream(read(inputStream).getBytes("UTF-8"));
+	public static WikiInputStream create(InputStream inputStream) throws IOException {
+		WikiInputStream wiki = new WikiInputStream();
+		wiki.readWikiText(inputStream);
+		wiki.finishWriting();
+		return wiki;
 	}
 
-	static String read(InputStream inputStream) throws IOException {
-		Pattern PATTERN = Pattern.compile("<jh>.*?</jh>", Pattern.DOTALL);
-		CharSequence contents = readFile(inputStream);
-		final StringBuilder jhText = new StringBuilder();
-		final Matcher matcher = PATTERN.matcher(contents);
+	private void readWikiText(InputStream input) throws IOException {
+		Pattern START_OR_END = Pattern.compile("(<jh>|</jh>)");
+		CharSequence contents = readFile(input);
+		final Matcher matcher = START_OR_END.matcher(contents);
+		int startTag = -1;
+		int startOfNonJh = 0;
 		while(matcher.find()) {
-			final String match = matcher.group();
-			jhText.append('\n');
-			jhText.append(match, 4, match.length() - 5); // strip tags
+			final int matchStart = matcher.start();
+			final int matchEnd = matcher.end();
+			final CharSequence matched = contents.subSequence(matchStart, matchEnd);
+			if ("<jh>".equals(matched)) {
+				if (startTag != -1) {
+					throw new RuntimeException(
+						"Found <jh> tag inside <jh> tag"
+					);
+				}
+				startTag = matchStart + matched.length();
+				findExpectedErrors(contents.subSequence(startOfNonJh, matchStart));
+			}
+			else {
+				if (startTag == -1) {
+					throw new RuntimeException(
+						"Found </jh> tag without matching <jh> tag");
+				}
+				buffer.append('\n');
+				buffer.append(contents.subSequence(startTag, matchStart));
+				startTag = -1;
+				startOfNonJh = matchStart + matched.length();
+			}
 		}
-		return jhText.toString();
+		if (startTag != -1) {
+			throw new RuntimeException(
+				"Missing </jh> tag"
+			);
+		}
+		findExpectedErrors(contents.subSequence(startOfNonJh, contents.length()));
+	}
+
+	static String read(String input) throws IOException {
+		return create(new ByteArrayInputStream(input.getBytes("UTF-8"))).getContents();
 	}
 
 	private static CharSequence readFile(InputStream inputStream) throws IOException {
@@ -74,4 +142,17 @@ private static CharSequence readFile(InputStream inputStream) throws IOException
 		return contents.toString("UTF-8");
 	}
 
+	private void findExpectedErrors(CharSequence wikiText) {
+		Pattern EXPECTED_ERRORS = Pattern.compile(
+			"\\{\\{\\s*error expected\\s*[|]\\s*([^|}]+)\\s*\\}\\}");
+		Matcher matcher = EXPECTED_ERRORS.matcher(wikiText);
+		while (matcher.find()) {
+			expectedErrors.add(matcher.group(1));
+		}
+	}
+
+	public List<String> expectedErrors() {
+		return expectedErrors;
+	}
+
 }

src/main/java/jhilbert/scanners/impl/StreamTokenFeed.java

@@ -34,7 +34,7 @@ See the commit logs ("git log") for a list of individual contributions.
 /**
  * A token feed for stream I/O.
  */
-final class StreamTokenFeed extends AbstractTokenFeed {
+class StreamTokenFeed extends AbstractTokenFeed {
 
 	/**
 	 * Logger for this class.

src/main/java/jhilbert/scanners/impl/WikiStreamTokenFeed.java

@@ -0,0 +1,54 @@
+/*
+    JHilbert, a verifier for collaborative theorem proving
+
+    Copyright © 2008, 2009, 2011 The JHilbert Authors
+      See the AUTHORS file for the list of JHilbert authors.
+      See the commit logs ("git log") for a list of individual contributions.
+
+    This program is free software: you can redistribute it and/or modify
+    it under the terms of the GNU General Public License as published by
+    the Free Software Foundation, either version 3 of the License, or
+    (at your option) any later version.
+
+    This program is distributed in the hope that it will be useful,
+    but WITHOUT ANY WARRANTY; without even the implied warranty of
+    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+    GNU General Public License for more details.
+
+    You should have received a copy of the GNU General Public License
+    along with this program.  If not, see <http://www.gnu.org/licenses/>.
+
+    You may contact the author on this Wiki page:
+    http://www.wikiproofs.de/w/index.php?title=User_talk:GrafZahl
+*/
+
+package jhilbert.scanners.impl;
+
+import java.io.InputStream;
+import java.util.ArrayList;
+import java.util.List;
+
+import jhilbert.scanners.ScannerException;
+
+/**
+ * A token feed for stream I/O.
+ */
+public class WikiStreamTokenFeed extends StreamTokenFeed {
+
+	List<String> rejections = new ArrayList<String>();
+
+	public WikiStreamTokenFeed(final InputStream in) throws ScannerException {
+		super(in);
+	}
+
+	public @Override void reject(final String msg) {
+		rejections.add(msg);
+		super.reject(msg);
+	}
+
+	public boolean hasRejection(String message) {
+		System.out.println(rejections);
+		return rejections.contains(message);
+	}
+
+}

src/main/java/jhilbert/storage/Storage.java

@@ -40,7 +40,7 @@ public abstract class Storage {
 	/**
 	 * Instance.
 	 */
-	private static final Storage instance;
+	private static Storage instance;
 
 	/**
 	 * Choose instance.
@@ -73,6 +73,10 @@ public static Storage getInstance() {
 		return instance;
 	}
 
+	public static void setInstance(Storage storage) {
+		instance = storage;
+	}
+
 	/**
 	 * Module cache.
 	 */

src/main/java/jhilbert/storage/hashstore/Storage.java

@@ -73,6 +73,7 @@ public final class Storage extends jhilbert.storage.Storage {
 	/**
 	 * Digest charset.
 	 */
+	@SuppressWarnings("unused")
 	private static final Charset HASHER_CHARSET = Charset.forName("UTF-8");
 
 	/**

src/main/java/jhilbert/storage/mediawiki/Storage.java

@@ -140,7 +140,6 @@ private RevisionHandler handleRequest(final String req) throws StorageException
 		assert (!"".equals(locator)): "Proof module supplied";
 		assert (revision >= 0): "Invalid version number supplied";
 		try {
-			final String urlEncodedLocator = URLEncoder.encode(locator, ENCODING);
 			final RevisionHandler handler = handleRequest("revids=" + revision + "&prop=revisions&rvprop=content");
 			if (!locator.equals(handler.getPageTitle()))
 				throw new StorageException("Supplied revision " + revision + " does not match supplied title " + locator);

src/main/java/jhilbert/storage/wiki/Storage.java

@@ -119,6 +119,8 @@ public final class Storage extends jhilbert.storage.Storage {
 	 */
 	public static String fileName(String jhilbertName) {
 		String[] parts = jhilbertName.split(":");
+		if (parts.length != 2)
+			throw new RuntimeException("Filename must contain exactly one colon: " + jhilbertName);
 		String namespace = parts[0];
 		String underscoredName = parts[1];