From 83612ae5ba285c7b83fefef9a9bb381166255386 Mon Sep 17 00:00:00 2001
From: Hans-Peter Deifel <hans-peter.deifel@fau.de>
Date: Tue, 21 Mar 2017 11:56:15 +0100
Subject: [PATCH] debugger: Stop and print result if reasoner finishes
The 'step' command takes an optional repeat count. Now it stops
stepping and prints the result if the reasoner finishes before
reaching the specified number of steps.
---
src/debugger/debugger.ml | 12 +++++++-----
1 file changed, 7 insertions(+), 5 deletions(-)
diff --git a/src/debugger/debugger.ml b/src/debugger/debugger.ml
index a1a1aaa..7f75b17 100644
--- a/src/debugger/debugger.ml
+++ b/src/debugger/debugger.ml
@@ -43,20 +43,22 @@ let printStatus () =
print_endline (CM.queuePrettyStatus ());
printResult ()
-let rec repeat (n:int) (action: unit -> unit) =
+(** Repeat either n times or until action returns true *)
+let rec repeat (n:int) (action: unit -> bool) =
if n <= 0
then ()
- else (action() ; repeat (n-1) action)
+ else (if action() then () else repeat (n-1) action)
let doStep args =
let action() =
if Reasoner.reasonerFinished ()
- then print_endline "Reasoner already finished!"
+ then (print_endline "Reasoner already finished!"; true)
else
try
Reasoner.runReasonerStep ();
- if (Reasoner.reasonerFinished ()) then printResult();
- with CoAlgMisc.CoAlg_finished _ -> printResult()
+ if (Reasoner.reasonerFinished ()) then (printResult(); true)
+ else false
+ with CoAlgMisc.CoAlg_finished _ -> (printResult(); true)
in
let steps = match args with
| (str::_) -> (int_of_string str)
--
GitLab