From 928f3d1e531bd8125b110597717b44d83d7f25ea Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Sat, 20 Jan 2007 15:16:55 +0000 Subject: [PATCH] An "assert false" used to be raised when matitac was started on an empty file. --- helm/software/matita/matitacLib.ml | 14 ++++++-------- 1 file changed, 6 insertions(+), 8 deletions(-) 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 -- 2.39.2