[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index] [List Home]
[imp-commit] r22964 - trunk/org.eclipse.imp.pdb.values/src/org/eclipse/imp/pdb/facts/io

Author: jvinju
Date: 2012-01-10 04:59:57 -0500 (Tue, 10 Jan 2012)
New Revision: 22964

Modified:
   trunk/org.eclipse.imp.pdb.values/src/org/eclipse/imp/pdb/facts/io/BinaryValueWriter.java
   trunk/org.eclipse.imp.pdb.values/src/org/eclipse/imp/pdb/facts/io/StandardTextWriter.java
Log:
added some judicious calls to Writer.flush() to prevent data-loss

Modified: trunk/org.eclipse.imp.pdb.values/src/org/eclipse/imp/pdb/facts/io/BinaryValueWriter.java
===================================================================
--- trunk/org.eclipse.imp.pdb.values/src/org/eclipse/imp/pdb/facts/io/BinaryValueWriter.java	2012-01-09 08:36:45 UTC (rev 22963)
+++ trunk/org.eclipse.imp.pdb.values/src/org/eclipse/imp/pdb/facts/io/BinaryValueWriter.java	2012-01-10 09:59:57 UTC (rev 22964)
@@ -48,6 +48,7 @@
 	public void write(IValue value, OutputStream outputStream) throws IOException{
 		BinaryWriter binaryWriter = new BinaryWriter(value, outputStream, new TypeStore());
 		binaryWriter.serialize();
+		outputStream.flush();
 	}
 	
 	/**
@@ -66,6 +67,7 @@
 	public void write(IValue value, OutputStream outputStream, TypeStore typeStore) throws IOException{
 		BinaryWriter binaryWriter = new BinaryWriter(value, outputStream, typeStore);
 		binaryWriter.serialize();
+		outputStream.flush();
 	}
 	
 	/**
@@ -87,6 +89,7 @@
 			
 			BinaryWriter binaryWriter = new BinaryWriter(value, fos, typeStore);
 			binaryWriter.serialize();
+			fos.flush();
 		}finally{
 			if(fos != null){
 				fos.close();

Modified: trunk/org.eclipse.imp.pdb.values/src/org/eclipse/imp/pdb/facts/io/StandardTextWriter.java
===================================================================
--- trunk/org.eclipse.imp.pdb.values/src/org/eclipse/imp/pdb/facts/io/StandardTextWriter.java	2012-01-09 08:36:45 UTC (rev 22963)
+++ trunk/org.eclipse.imp.pdb.values/src/org/eclipse/imp/pdb/facts/io/StandardTextWriter.java	2012-01-10 09:59:57 UTC (rev 22964)
@@ -61,8 +61,12 @@
 	public void write(IValue value, java.io.Writer stream) throws IOException {
 		try {
 			value.accept(new Writer(stream, indent, tabSize));
-		} catch (VisitorException e) {
+		} 
+		catch (VisitorException e) {
 			throw (IOException) e.getCause();
+		} 
+		finally {
+			stream.flush();
 		}
 	}