From fa077ec417f06b3785ef4ce629f793ce8e8b3690 Mon Sep 17 00:00:00 2001 From: Andrei Paskevich Date: Thu, 21 Mar 2013 11:10:12 +0100 Subject: [PATCH] fix why3session.dtd --- .../logic/triangle_inequality/why3session.xml | 622 ++++++++---------- share/why3session.dtd | 9 +- src/session/session.ml | 19 +- 3 files changed, 293 insertions(+), 357 deletions(-) diff --git a/examples/logic/triangle_inequality/why3session.xml b/examples/logic/triangle_inequality/why3session.xml index a9857010d..94d62b8e6 100644 --- a/examples/logic/triangle_inequality/why3session.xml +++ b/examples/logic/triangle_inequality/why3session.xml @@ -28,13 +28,9 @@ - - - - - - - - - - - - + + + - - + + + - - + + + - - + + + - - + + + - - + + + - - + + + - - + + + - - + + + - - + + + - - + + + - - - + + + + - - - + + + + - - - + + + + - - - + + + + - - - + + + + - - - - + + + + + - - - + + + + - - + + + - - + + + - - - + + + + - - + + + - - + + + - - + + + - - + + + - - + + + - - + + + - - + + + - - + + + - - + + + - - + + + - - + + + - - + + + - - + + + - - + + + - - + + + - - + + + - - + + + - - + + + - - + + + - - + + + - + + - + + - + + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - - - - - - - - - - - - - + - + - - + - + diff --git a/src/session/session.ml b/src/session/session.ml index dbba1228e..084f278a9 100644 --- a/src/session/session.ml +++ b/src/session/session.ml @@ -558,26 +558,25 @@ and save_metas provers fmt _ m = fprintf fmt "@\n@[" m.metas_verified m.metas_expanded; let save_pos fmt pos = - fprintf fmt "@\n@[ip_theory=\"%a\">" save_string pos.ip_theory; + fprintf fmt "ip_theory=\"%a\">" save_string pos.ip_theory; List.iter (fprintf fmt "@\n@[@]" save_string) pos.ip_library; List.iter (fprintf fmt "@\n@[@]" save_string) pos.ip_qualid; - fprintf fmt "@]"; in let save_ts_pos fmt ts pos = fprintf fmt "@\n@[@]" + id=\"%i\"@ %a@]@\n" save_string ts.ts_name.id_string (List.length ts.ts_args) (ts_hash ts) save_pos pos in let save_ls_pos fmt ls pos = (** TODO: add the signature? *) - fprintf fmt "@\n@[@]" + fprintf fmt "@\n@[" save_string ls.ls_name.id_string (ls_hash ls) save_pos pos in let save_pr_pos fmt pr pos = - fprintf fmt "@\n@[@]" + fprintf fmt "@\n@[" save_string pr.pr_name.id_string (pr_hash pr) save_pos pos in @@ -1888,7 +1887,7 @@ and merge_trans ~keygen ~theories env to_goal _ from_transf = with Exit -> () -(** convert the ident from the olf task to the ident at the same +(** convert the ident from the old task to the ident at the same position in the new task *) and merge_metas_aux ~keygen ~theories env to_goal _ from_metas = (** Find in the new task the new symbol (ts,ls,pr) *) @@ -1907,11 +1906,9 @@ and merge_metas_aux ~keygen ~theories env to_goal _ from_metas = let rec read_theory ip = function | [] -> raise (Env.LibFileNotFound ip.ip_library) | format::formats -> - try - Env.read_theory ~format env.env - ip.ip_library ip.ip_theory - with Env.LibFileNotFound _ | Env.TheoryNotFound _ -> - read_theory ip formats + try Env.read_theory ~format env.env ip.ip_library ip.ip_theory + with Env.LibFileNotFound _ | Env.TheoryNotFound _ -> + read_theory ip formats in let read_theory ip = if ip.ip_library = [] then Mstr.find ip.ip_theory theories -- 2.24.1