Skip to content

Commit

Permalink
Fix JS worker
Browse files Browse the repository at this point in the history
  • Loading branch information
Halbaroth committed Apr 19, 2023
1 parent e2cba0f commit 6d9f549
Show file tree
Hide file tree
Showing 11 changed files with 278 additions and 272 deletions.
14 changes: 7 additions & 7 deletions src/bin/common/solving_loop.ml
Original file line number Diff line number Diff line change
Expand Up @@ -270,11 +270,11 @@ let main () =
in

(* let all_used_context = FE.init_all_used_context () in
if Options.get_timelimit_per_goal() then
FE.print_status FE.Preprocess 0;
let assertion_stack = Stack.create () in
let typing_loop state p =
if get_parse_only () then state else begin
if Options.get_timelimit_per_goal() then
FE.print_status FE.Preprocess 0;
let assertion_stack = Stack.create () in
let typing_loop state p =
if get_parse_only () then state else begin
try
let l, env = I.type_parsed state.env assertion_stack p in
let used_names = I.get_env_logics state.env in
Expand All @@ -285,8 +285,8 @@ let main () =
if e != Warning_as_error then
Printer.print_err "%a" Errors.report e;
exit 1
end
in *)
end
in *)

let handle_stmt :
FE.used_context -> State.t ->
Expand Down
2 changes: 1 addition & 1 deletion src/bin/gui/annoted_ast.ml
Original file line number Diff line number Diff line change
Expand Up @@ -1841,7 +1841,7 @@ let rec add_atyped_decl errors (buffer:sbuffer) ?(indent=0) ?(tags=[]) d =
| _ -> AFop (AOPnot, [aaform])
in
let goal_str =
match (gs : Typed.goal_sort) with
match (gs : Ty.goal_sort) with
| Thm -> "check valid"
| Sat -> "check sat"
| AllSat l ->
Expand Down
Loading

0 comments on commit 6d9f549

Please sign in to comment.