Browse Source

explicit.ExportIterations: add flush() for useful iterations.html

If there are exceptions during the iteration, we want to have a working HTML file with the iterations up to that point.

By flushing after each vector, we can ensure that the HTML is in a working state.
master
Joachim Klein 8 years ago
committed by GitHub
parent
commit
90fa90e5da
No known key found for this signature in database GPG Key ID: 4AEE18F83AFDEB23
  1. 4
      prism/src/explicit/ExportIterations.java

4
prism/src/explicit/ExportIterations.java

@ -67,6 +67,7 @@ public class ExportIterations {
log.println("<h1>" + title + "</h1>");
log.println("<svg></svg>");
log.println("<script src=\"http://www.prismmodelchecker.org/js/res/iteration-vis-v1.js\"></script>");
log.flush();
}
/**
@ -92,6 +93,7 @@ public class ExportIterations {
exportValue(d);
}
log.print("]," + type + ")</script>\n");
log.flush();
}
/**
@ -117,6 +119,7 @@ public class ExportIterations {
exportValue(d);
}
log.print("]," + type + ")</script>\n");
log.flush();
}
private void exportValue(double d)
@ -134,6 +137,7 @@ public class ExportIterations {
public void close()
{
log.println("\n</body></html>");
log.flush();
}
public static void setDefaultFilename(String newDefaultFilename)

Loading…
Cancel
Save