From 86152c374baac127fe5a4bbe7a92f1ffd4a0aaa8 Mon Sep 17 00:00:00 2001
From: "Achim D. Brucker" <adbrucker@0x5f.org>
Date: Mon, 27 Feb 2023 08:39:53 +0000
Subject: [PATCH] Initial implementation of list_templates and list_ontologies
 (fixes #28).

---
 Isabelle_DOF/thys/Isa_DOF.thy | 31 ++++++++++++++++++++++++++++++-
 scala/dof_mkroot.scala        |  2 ++
 2 files changed, 32 insertions(+), 1 deletion(-)

diff --git a/Isabelle_DOF/thys/Isa_DOF.thy b/Isabelle_DOF/thys/Isa_DOF.thy
index 191c937..64d9040 100644
--- a/Isabelle_DOF/thys/Isa_DOF.thy
+++ b/Isabelle_DOF/thys/Isa_DOF.thy
@@ -46,7 +46,8 @@ theory Isa_DOF                (* Isabelle Document Ontology Framework *)
   and      "use_template" "use_ontology"         :: thy_decl
   and      "define_template" "define_ontology"           :: thy_load
   and      "print_doc_classes"        "print_doc_items" 
-           "print_doc_class_template" "check_doc_global" :: diag
+           "print_doc_class_template" "check_doc_global"
+           "list_ontologies" "list_templates"  :: diag
 
       
 
@@ -3039,6 +3040,8 @@ sig
   val define_ontology: binding * string -> theory -> string * theory
   val use_template: Context.generic -> xstring * Position.T -> unit
   val use_ontology: Context.generic -> (xstring * Position.T) list -> unit
+  val list_ontologies: Context.generic -> unit
+  val list_templates: Context.generic -> unit
 end;
 
 structure Document_Context: DOCUMENT_CONTEXT =
@@ -3090,6 +3093,7 @@ fun strip prfx sffx (path, pos) =
 
 in
 
+
 val template_space = get_space fst;
 val ontology_space = get_space snd;
 
@@ -3116,6 +3120,20 @@ fun use_ontology context args =
 val strip_template = strip "root-" ".tex";
 val strip_ontology = strip "DOF-" ".sty";
 
+
+fun list_ontologies context = 
+    let 
+       val names = ((Name_Space.get_names o ontology_space) context)
+       val fq_names = map (fn n => ((Long_Name.base_name o Long_Name.qualifier) n)^"."^(Long_Name.base_name n)) names
+       val _ = map writeln fq_names
+    in () end
+
+fun list_templates context = 
+    let 
+       val full_names = ((Name_Space.get_names o template_space) context)
+       val _ = map (writeln o  Long_Name.base_name) full_names
+    in ()  end
+
 end;
 
 
@@ -3155,6 +3173,17 @@ val _ =
           val text = cat_lines (#lines file);
         in #2 (define_ontology (binding, text) thy') end)));
 
+val _ =
+  Outer_Syntax.command \<^command_keyword>\<open>list_templates\<close>
+    "list available DOF document templates (as defined within theory context)"
+    (Scan.succeed (Toplevel.theory (fn thy => (list_templates (Context.Theory thy); thy))));
+
+val _ =
+  Outer_Syntax.command \<^command_keyword>\<open>list_ontologies\<close>
+    "list available DOF document ontologies (as defined within theory context)"
+    (Scan.succeed (Toplevel.theory (fn thy => (list_ontologies (Context.Theory thy); thy))));
+
+
 end;
 \<close>
 
diff --git a/scala/dof_mkroot.scala b/scala/dof_mkroot.scala
index c600909..96ee62a 100644
--- a/scala/dof_mkroot.scala
+++ b/scala/dof_mkroot.scala
@@ -90,7 +90,9 @@ object DOF_Mkroot
       "\nimports\n  " + ontologies.map("Isabelle_DOF." + _).mkString("\n  ") +  """
 begin
 
+list_templates
 use_template """ + quote(template) + """
+list_ontologies
 use_ontology """ + ontologies.map(quote).mkString(" and ") + """
 
 end