(* ~/src/Tools/isac/BridgeLibisabelle/pbl-met-hierarchy.sml

   author: Walther Neuper 2004

   (c) isac-team

Create XML for the tree structure of problem-patterns and methods.

This is kept as a model for some browsing facility, which is required

in parallel to PIDE, because these structures are different

from the dependency graph of Isabelle's theories.

*)

signature PROBLEM_METHOD_HIERARCHY =

sig

  eqtype filepath

  eqtype filename

  type xml

  val pbl_hierarchy2file : filepath -> filepath * string

  val met_hierarchy2file : filepath -> filepath * string

  val pbl_hierarchy2file_test : filepath -> filepath * string

  val met_hierarchy2file_test : filepath -> filepath * string

  val update_metpair: theory -> MethodC.id -> Error_Pattern.T list -> MethodC.T * MethodC.id

end

(**)

structure Pbl_Met_Hierarchy(**): PROBLEM_METHOD_HIERARCHY(*AUTHOR*) =

struct

(**)

type filepath = string;

type filename = string;

type xml = string; (* rm together with old code replaced by XML.tree *)

val indentation = 2;

fun hierarchy_pbl h =

  let

    val j = indentation

    fun nd i p (Store.Node (id,[{guh,...} : Problem.T],ns)) = 

        let val p' = Pos.lev_on p

        in (indt i) ^ "<NODE>\n" ^ 

           (indt (i+j)) ^ "<ID> " ^ id ^ " </ID>\n" ^ 

           (indt (i+j)) ^ "<NO> " (*on this level*) ^ 

           (string_of_int o last_elem) p' ^ " </NO>\n" ^ 

           (indt (i+j)) ^ "<CONTENTREF> " ^ guh ^ 

           " </CONTENTREF>\n" ^

           (nds (i+j) (Pos.lev_dn p') ns) ^ 

           (indt i) ^ "</NODE>\n"

        end

      | nd _ _ _ = raise ERROR "hierarchy_pbl"

    and nds _ _ [] = "" 

      | nds i p (n::ns) = (nd i p n) ^ (nds i (Pos.lev_on p) ns);

  in nds j [0] h : xml end;

fun hierarchy_met h =

  let

    val j = indentation

	  fun nd i p (Store.Node (id,[{guh,...} : MethodC.T],ns)) = 

  	    let val p' = Pos.lev_on p

  	    in (indt i) ^ "<NODE>\n" ^ 

  	       (indt (i+j)) ^ "<ID> " ^ id ^ " </ID>\n" ^ 

  	       (indt (i+j)) ^ "<NO> " (*on this level*) ^ 

  	       (string_of_int o last_elem) p' ^ " </NO>\n" ^ 

  	       (indt (i+j)) ^ "<CONTENTREF> " ^ guh ^ 

  	       " </CONTENTREF>\n" ^

  	       (nds (i+j) (Pos.lev_dn p') ns) ^ 

  	       (indt i) ^ "</NODE>\n"

  	    end

      | nd _ _ _ = raise ERROR "hierarchy_met"

	  and nds _ _ [] = ""

	    | nds i p (n::ns) = (nd i p n) ^ (nds i (Pos.lev_on p) ns);

  in nds j [0] h  : xml end;

(*

fun str2file (fnm : filename) (str : string) =

  let val file = TextIO.openOut fnm

  in 

    TextIO.output (file, str);

    TextIO.flushOut file;

    TextIO.closeOut file

  end

*)

(* files *all* problems addressed by the context of the test run *)

fun pbl_hierarchy2file path = 

    (*str2file*) (path ^ "pbl_hierarchy.xml" : filepath,

	      "<NODE>\n" ^

	      "  <ID> problem hierarchy </ID>\n" ^

	      "  <NO> 1 </NO>\n" ^

	      "  <CONTENTREF> pbl_ROOT </CONTENTREF>\n" ^

	     (hierarchy_pbl (get_pbls ())) ^

	     "</NODE>");

(* some tests extend the hierarchy_pbl, but these shall not be shown *)

fun pbl_hierarchy2file_test path = 

    (*str2file*) (path ^ "pbl_hierarchy.xml" : filepath,

	      "<NODE>\n" ^

	      "  <ID> problem hierarchy </ID>\n" ^

	      "  <NO> 1 </NO>\n" ^

	      "  <CONTENTREF> pbl_ROOT </CONTENTREF>\n" ^

	     ("Isac_Knowledge" |> Know_Store.get_via_last_thy |> Know_Store.get_pbls |> hierarchy_pbl) ^

	     "</NODE>");

(* files *all* methods addressed by the context of the test run *)

fun met_hierarchy2file path = 

    (*str2file*) (path ^ "met_hierarchy.xml" : filepath,

	      "<NODE>\n" ^

	      "  <ID> method hierarchy </ID>\n" ^

	      "  <NO> 1 </NO>\n" ^

	      "  <CONTENTREF> met_ROOT </CONTENTREF>\n" ^

	     (hierarchy_met (get_mets ())) ^

	     "</NODE>");

(* some tests extend the hierarchy_met, but these shall not be shown *)

fun met_hierarchy2file_test path = 

    (*str2file*) (path ^ "met_hierarchy.xml" : filepath,

	      "<NODE>\n" ^

	      "  <ID> method hierarchy </ID>\n" ^

	      "  <NO> 1 </NO>\n" ^

	      "  <CONTENTREF> met_ROOT </CONTENTREF>\n" ^

	     ("Isac_Knowledge" |> Know_Store.get_via_last_thy |> Know_Store.get_mets |> hierarchy_met) ^

	     "</NODE>");

fun update_metdata

  ({guh, mathauthors, start_refine, rew_ord, asm_rls, prog_rls, where_rls, rew_rls, calc, model,

      where_, program, ...}: MethodC.T) errpats' =

  {guh = guh, mathauthors = mathauthors, start_refine = start_refine, rew_ord = rew_ord,

    asm_rls = asm_rls, prog_rls = prog_rls, where_rls = where_rls, rew_rls = rew_rls, calc = calc,

    model = model, where_ = where_, program = program, errpats = errpats'}: MethodC.T

(* interface for dialog-authoring: call in Buld_Thydata.thy only ! *)

fun update_metpair thy metID errpats =

  let

    val ret = (update_metdata (MethodC.from_store' thy metID) errpats, metID)

      handle ERROR _ => raise ERROR ("update_metpair: " ^ strs2str metID ^ " must address a method");

  in ret end;

(**)end(**)