From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Sat, 20 Jan 2007 15:16:55 +0000 (+0000)
Subject: An "assert false" used to be raised when matitac was started on an empty file.
X-Git-Tag: make_still_working~6516
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=928f3d1e531bd8125b110597717b44d83d7f25ea;p=helm.git

An "assert false" used to be raised when matitac was started on an empty file.
---

diff --git a/helm/software/matita/matitacLib.ml b/helm/software/matita/matitacLib.ml
index cb3b2d1c8..ba9af1302 100644
--- a/helm/software/matita/matitacLib.ml
+++ b/helm/software/matita/matitacLib.ml
@@ -65,14 +65,12 @@ let run_script is eval_function  =
   in
   let matita_debug = Helm_registry.get_bool "matita.debug" in
   try
-   let grafite_status'', lexicon_status'' =
-    match eval_function lexicon_status' grafite_status' is cb with
-       [] -> assert false
-     | (s,None)::_ -> s
-     | (s,Some _)::_ -> raise AttemptToInsertAnAlias
-   in
-    lexicon_status := Some lexicon_status'';
-    grafite_status := Some grafite_status''
+   match eval_function lexicon_status' grafite_status' is cb with
+      [] -> raise End_of_file
+    | ((grafite_status'',lexicon_status''),None)::_ ->
+       lexicon_status := Some lexicon_status'';
+       grafite_status := Some grafite_status''
+    | (s,Some _)::_ -> raise AttemptToInsertAnAlias
   with
   | GrafiteEngine.Drop  
   | End_of_file