(* Title:  BridgeLibisabelle/present-tool.sml

    Author: Walther Neuper

    (c) due to copyright terms

 This code remains in order to

 keep tests of interaction Java-frontend <-> Kernel running.

 *)

 signature PRESENTATION_TOOL =

 sig

   type ketype

   val ketype2str: ketype -> string

   val str2ketype': string -> ketype

   type kestoreID

   val pblID2guh : Proof.context -> Problem.id -> Check_Unique.id

   val metID2guh : (*Proof.context ->*) MethodC.id -> Check_Unique.id

   val kestoreID2guh : Proof.context -> ketype -> kestoreID -> Check_Unique.id

   val guh2kestoreID : Check_Unique.id -> string list

 end

 (**)

 structure Ptool(**) : PRESENTATION_TOOL(**) =

 struct

 (**)

 (* lookup a guh in hierarchy of problems / methods depending on fst 4 chars in guh *)

 fun guh2kestoreID guh =

   case (implode o (take_fromto 1 4) o Symbol.explode) guh of

 	  "pbl_" =>

 	    let

 	      fun node ids gu (Store.Node (id, [{guh, ...}], ns)) =

 	        if gu = guh then SOME (ids @ [id]) else nodes (ids @ [id]) gu ns

 	        | node _ _ _ = raise ERROR "Ptool.guh2kestoreID node: uncovered fun def."

 	      and nodes _ _ [] = NONE 

 	        | nodes ids gu (n :: ns) = case node ids gu n of

 	            SOME id => SOME id

 			      | NONE =>  nodes ids gu ns

 	    in case nodes [] guh (get_pbls ()) of

 	      SOME id => rev id

 	    | NONE => raise ERROR ("Ptool.guh2kestoreID: \"" ^ guh ^ "\" " ^ "not found in ptyps")

       end

   | "met_" =>

 	    let

 	      fun node ids gu (Store.Node (id, [{guh, ...}], ns)) =

 	        if gu = guh then SOME (ids @ [id]) else nodes (ids @ [id]) gu ns

 	        | node _ _ _ = raise ERROR "Ptool.guh2kestoreID node: uncovered fun def."

 	      and nodes _ _ [] = NONE 

 	        | nodes ids gu (n :: ns) = case node ids gu n of

 	            SOME id => SOME id

 				    | NONE =>  nodes ids gu ns

 	    in case nodes [] guh (get_mets ()) of

 	      SOME id => id

 	    | NONE => raise ERROR ("Ptool.guh2kestoreID: \"" ^ guh ^ "\" " ^ "not found in mets")

       end

   | _ => raise ERROR ("Ptool.guh2kestoreID called with \"" ^ guh ^ "\":");

 (* for distinction of contexts WN130621: disambiguate with Isabelle's Context *)

 datatype ketype = Exp_ | Thy_ | Pbl_ | Met_;

 fun ketype2str Exp_ = "Exp_"

   | ketype2str Thy_ = "Thy_"

   | ketype2str Pbl_ = "Pbl_"

   | ketype2str Met_ = "Met_";

 (* for conversion from XML *)

 fun str2ketype' "exp" = Exp_

   | str2ketype' "thy" = Thy_

   | str2ketype' "pbl" = Pbl_

   | str2ketype' "met" = Met_

   | str2ketype' str = raise ERROR ("str2ketype': WRONG arg = " ^ str)

 (*either ThyC.id or Problem.id or MethodC.id*)

 type kestoreID = string list;

 (* make a guh from a reference to an element in the kestore;

    EXCEPT theory hierarchy ... compare 'fun keref2xml'    *)

 fun pblID2guh ctxt pblID = (((#guh o (Problem.from_store ctxt)) pblID)

   handle ERROR _ => raise ERROR ("Ptool.pblID2guh: not for \"" ^ strs2str' pblID ^ "\""));

 fun metID2guh metID =

   (((#guh o MethodC.from_store ("Isac_Knowledge" |> Know_Store.get_via_last_thy |> Proof_Context.init_global)) metID)

   handle ERROR _ => raise ERROR ("metID2guh: no 'Met_' for \"" ^ strs2str' metID ^ "\""));

 fun kestoreID2guh ctxt Pbl_ kestoreID = pblID2guh ctxt kestoreID

   | kestoreID2guh _ Met_ kestoreID = metID2guh kestoreID

   | kestoreID2guh _ ketyp kestoreID =

     raise ERROR ("kestoreID2guh: \"" ^ ketype2str ketyp ^ "\" not for \"" ^ strs2str' kestoreID ^ "\"");

 (**)end(**);