From 058c49a51d9bf05a6e45dfad5806bfaf94101d74 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Tuong?=
<tuong@users.noreply.github.com>
Date: Sat, 9 May 2020 12:13:41 +0000
Subject: [PATCH] move sessions to a separate directory
git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@14183 3260e6d1-4efc-4170-b0a7-36055960796d
---
Citadelle/ROOT | 3 ++
Citadelle/examples/C_Model_core.thy | 2 +-
Citadelle/examples/C_Model_init.thy | 2 +-
.../compiler/Generator_dynamic_concurrent.thy | 2 +-
.../Generator_dynamic_export_testing.thy | 2 +-
.../compiler/Generator_dynamic_sequential.thy | 2 +-
Citadelle/src/compiler/core/Core_init.thy | 2 +-
Citadelle/src/compiler/meta/Meta_HKB.thy | 2 +-
Citadelle/src/compiler/meta/Meta_META.thy | 2 +-
Citadelle/src/compiler/meta/Meta_UML.thy | 4 +--
.../src/compiler/meta/Meta_UML_extended.thy | 2 +-
Citadelle/src/compiler/meta/Parser_HKB.thy | 2 +-
Citadelle/src/compiler/meta/Parser_META.thy | 2 +-
Citadelle/src/compiler/meta/Parser_UML.thy | 2 +-
.../src/compiler/meta/Parser_UML_extended.thy | 2 +-
Citadelle/src/compiler/meta/Printer_META.thy | 2 +-
Citadelle/src/compiler/meta/Printer_UML.thy | 2 +-
Citadelle/src/compiler_generic/ROOT | 34 -------------------
Citadelle/src/uml_ocl/UML_OCL.thy | 2 +-
19 files changed, 21 insertions(+), 52 deletions(-)
diff --git a/Citadelle/ROOT b/Citadelle/ROOT
index 8e1d225ce4e..988554ce8e6 100644
--- a/Citadelle/ROOT
+++ b/Citadelle/ROOT
@@ -72,6 +72,9 @@ session FOCL in "src/uml_ocl" = "HOL-Library" +
options [document=pdf,document_output=document_generated,
document_variants="document=noexample,-afp,-annexa",
show_question_marks = false]
+ sessions
+ OCL
+ Isabelle_Meta_Model
theories
UML_OCL
document_files
diff --git a/Citadelle/examples/C_Model_core.thy b/Citadelle/examples/C_Model_core.thy
index b547e33bafb..6a56654ffec 100644
--- a/Citadelle/examples/C_Model_core.thy
+++ b/Citadelle/examples/C_Model_core.thy
@@ -38,7 +38,7 @@
theory C_Model_core
imports "$HASKABELLE_HOME_USER/default/Prelude"
- FOCL.UML_Main
+ OCL.UML_Main
Citadelle.Generator_dynamic_concurrent
Citadelle_C_init.C_Model_init
begin
diff --git a/Citadelle/examples/C_Model_init.thy b/Citadelle/examples/C_Model_init.thy
index 2f90a2d035d..b39139d1cd9 100644
--- a/Citadelle/examples/C_Model_init.thy
+++ b/Citadelle/examples/C_Model_init.thy
@@ -37,7 +37,7 @@
******************************************************************************)
theory C_Model_init
- imports FOCL.Printer_init
+ imports Isabelle_Meta_Model.Printer_init
Citadelle.Old_Datatype
begin
diff --git a/Citadelle/src/compiler/Generator_dynamic_concurrent.thy b/Citadelle/src/compiler/Generator_dynamic_concurrent.thy
index 4a0e939e8ba..508812a4714 100644
--- a/Citadelle/src/compiler/Generator_dynamic_concurrent.thy
+++ b/Citadelle/src/compiler/Generator_dynamic_concurrent.thy
@@ -43,7 +43,7 @@ section\<open>Dynamic Meta Embedding with Reflection\<close>
theory Generator_dynamic_concurrent
imports FOCL.Printer
- FOCL.Isabelle_typedecl
+ Isabelle_Meta_Model.Isabelle_typedecl
"~~/src/HOL/Library/Old_Datatype"
keywords (* OCL (USE tool) *)
"Between"
diff --git a/Citadelle/src/compiler/Generator_dynamic_export_testing.thy b/Citadelle/src/compiler/Generator_dynamic_export_testing.thy
index 3bd4452f359..0fadcb684a0 100644
--- a/Citadelle/src/compiler/Generator_dynamic_export_testing.thy
+++ b/Citadelle/src/compiler/Generator_dynamic_export_testing.thy
@@ -43,7 +43,7 @@ section\<open>Dynamic Meta Embedding with Reflection\<close>
theory Generator_dynamic_export_testing
imports FOCL.Printer
- FOCL.Isabelle_typedecl
+ Isabelle_Meta_Model.Isabelle_typedecl
"~~/src/HOL/Library/Old_Datatype"
keywords (* OCL (USE tool) *)
"Between"
diff --git a/Citadelle/src/compiler/Generator_dynamic_sequential.thy b/Citadelle/src/compiler/Generator_dynamic_sequential.thy
index ed31d334803..3bd69c83e80 100644
--- a/Citadelle/src/compiler/Generator_dynamic_sequential.thy
+++ b/Citadelle/src/compiler/Generator_dynamic_sequential.thy
@@ -43,7 +43,7 @@ section\<open>Dynamic Meta Embedding with Reflection\<close>
theory Generator_dynamic_sequential
imports Printer
- "../compiler_generic/isabelle_home/src/Pure/Isar/Isabelle_typedecl"
+ Isabelle_Meta_Model.Isabelle_typedecl
keywords (* OCL (USE tool) *)
"Between"
"Attributes" "Operations" "Constraints"
diff --git a/Citadelle/src/compiler/core/Core_init.thy b/Citadelle/src/compiler/core/Core_init.thy
index a5dc319fb74..581656eaa09 100644
--- a/Citadelle/src/compiler/core/Core_init.thy
+++ b/Citadelle/src/compiler/core/Core_init.thy
@@ -331,7 +331,7 @@ As general remark, all the future translating steps
will extensively use Isabelle expressions,
represented by its Meta-Model, for example lots of functions will use @{term "Term_app"}...
So the overall can be simplified by the use of polymorphic cartouches.
-It looks feasible to add a new front-end for cartouches in @{theory "FOCL.Init"}
+It looks feasible to add a new front-end for cartouches in @{theory "Isabelle_Meta_Model.Init"}
supporting the use of Isabelle syntax in cartouches,
then we could obtain at the end a parsed Isabelle Meta-Model in Isabelle.\<close>
diff --git a/Citadelle/src/compiler/meta/Meta_HKB.thy b/Citadelle/src/compiler/meta/Meta_HKB.thy
index 607922de053..b6396cd48ac 100644
--- a/Citadelle/src/compiler/meta/Meta_HKB.thy
+++ b/Citadelle/src/compiler/meta/Meta_HKB.thy
@@ -39,7 +39,7 @@
section\<open>Isabelle Meta-Model aka. AST definition of Isabelle\<close>
theory Meta_HKB
-imports "../../compiler_generic/Init"
+imports Isabelle_Meta_Model.Init
begin
section \<open>Miscellaneous\<close>
diff --git a/Citadelle/src/compiler/meta/Meta_META.thy b/Citadelle/src/compiler/meta/Meta_META.thy
index 6a9a5ba4ce8..e9711d823ef 100644
--- a/Citadelle/src/compiler/meta/Meta_META.thy
+++ b/Citadelle/src/compiler/meta/Meta_META.thy
@@ -45,7 +45,7 @@ theory Meta_META
imports Meta_UML
Meta_UML_extended
Meta_HKB
- "../../compiler_generic/meta_isabelle/Meta_Isabelle"
+ Isabelle_Meta_Model.Meta_Isabelle
begin
subsection\<open>A Basic Meta-Model\<close>
diff --git a/Citadelle/src/compiler/meta/Meta_UML.thy b/Citadelle/src/compiler/meta/Meta_UML.thy
index ee8b3258d66..94ece8b657c 100644
--- a/Citadelle/src/compiler/meta/Meta_UML.thy
+++ b/Citadelle/src/compiler/meta/Meta_UML.thy
@@ -42,8 +42,8 @@
section\<open>OCL Meta-Model aka. AST definition of OCL (I)\<close>
theory Meta_UML
-imports "../../compiler_generic/meta_isabelle/Meta_Pure"
- "../Init_rbt"
+imports Isabelle_Meta_Model.Meta_Pure
+ Isabelle_Meta_Model.Init_rbt
begin
subsection\<open>Type Definition\<close>
diff --git a/Citadelle/src/compiler/meta/Meta_UML_extended.thy b/Citadelle/src/compiler/meta/Meta_UML_extended.thy
index 2bd589496b9..6c2f0674ee0 100644
--- a/Citadelle/src/compiler/meta/Meta_UML_extended.thy
+++ b/Citadelle/src/compiler/meta/Meta_UML_extended.thy
@@ -42,7 +42,7 @@
section\<open>OCL Meta-Model aka. AST definition of OCL (II)\<close>
theory Meta_UML_extended
-imports "../../compiler_generic/Init"
+imports Isabelle_Meta_Model.Init
begin
subsection\<open>Type Definition\<close>
diff --git a/Citadelle/src/compiler/meta/Parser_HKB.thy b/Citadelle/src/compiler/meta/Parser_HKB.thy
index fbd32ed750a..31cf1943d6d 100644
--- a/Citadelle/src/compiler/meta/Parser_HKB.thy
+++ b/Citadelle/src/compiler/meta/Parser_HKB.thy
@@ -39,7 +39,7 @@ section\<open>Instantiating the Parser of Haskabelle\<close>
theory Parser_HKB
imports Meta_HKB
- "../../compiler_generic/meta_isabelle/Parser_init"
+ Isabelle_Meta_Model.Parser_init
begin
subsection\<open>Main\<close>
diff --git a/Citadelle/src/compiler/meta/Parser_META.thy b/Citadelle/src/compiler/meta/Parser_META.thy
index 5b1e9fc5edd..69fa97a586c 100644
--- a/Citadelle/src/compiler/meta/Parser_META.thy
+++ b/Citadelle/src/compiler/meta/Parser_META.thy
@@ -164,7 +164,7 @@ section\<open>Finalizing the Parser\<close>
text\<open>It should be feasible to invent a meta-command (e.g., @{text "datatype'"})
to automatically generate the previous recursors in @{text Parse}.
-Otherwise as an extra check, one can also overload polymorphic cartouches in @{theory FOCL.Init}
+Otherwise as an extra check, one can also overload polymorphic cartouches in @{theory Isabelle_Meta_Model.Init}
to really check that all the given constructor exists at the time of editing
(similarly as writing @{verbatim "@{term ...}"},
when it is embedded in a @{verbatim "text"} command).\<close>
diff --git a/Citadelle/src/compiler/meta/Parser_UML.thy b/Citadelle/src/compiler/meta/Parser_UML.thy
index 0621e0f480d..e7da7299512 100644
--- a/Citadelle/src/compiler/meta/Parser_UML.thy
+++ b/Citadelle/src/compiler/meta/Parser_UML.thy
@@ -43,7 +43,7 @@ section\<open>Instantiating the Parser of OCL (I)\<close>
theory Parser_UML
imports Meta_UML
- "../../compiler_generic/meta_isabelle/Parser_Pure"
+ Isabelle_Meta_Model.Parser_Pure
begin
subsection\<open>Building Recursors for Records\<close> (* NOTE part to be automated *)
diff --git a/Citadelle/src/compiler/meta/Parser_UML_extended.thy b/Citadelle/src/compiler/meta/Parser_UML_extended.thy
index 0b5fe8b9aaa..fbbad2e5955 100644
--- a/Citadelle/src/compiler/meta/Parser_UML_extended.thy
+++ b/Citadelle/src/compiler/meta/Parser_UML_extended.thy
@@ -43,7 +43,7 @@ section\<open>Instantiating the Parser of OCL (II)\<close>
theory Parser_UML_extended
imports Meta_UML_extended
- "../../compiler_generic/meta_isabelle/Parser_init"
+ Isabelle_Meta_Model.Parser_init
begin
subsection\<open>Building Recursors for Records\<close> (* NOTE part to be automated *)
diff --git a/Citadelle/src/compiler/meta/Printer_META.thy b/Citadelle/src/compiler/meta/Printer_META.thy
index c0e6d9062bf..74af181fdd6 100644
--- a/Citadelle/src/compiler/meta/Printer_META.thy
+++ b/Citadelle/src/compiler/meta/Printer_META.thy
@@ -43,7 +43,7 @@ section\<open>Instantiating the Printer for META\<close>
theory Printer_META
imports Parser_META
- "../../compiler_generic/meta_isabelle/Printer_Isabelle"
+ Isabelle_Meta_Model.Printer_Isabelle
Printer_UML_extended
begin
diff --git a/Citadelle/src/compiler/meta/Printer_UML.thy b/Citadelle/src/compiler/meta/Printer_UML.thy
index 39e9fffb29e..4346a73c246 100644
--- a/Citadelle/src/compiler/meta/Printer_UML.thy
+++ b/Citadelle/src/compiler/meta/Printer_UML.thy
@@ -43,7 +43,7 @@ section\<open>Instantiating the Printer for OCL (I)\<close>
theory Printer_UML
imports Meta_UML
- "../../compiler_generic/meta_isabelle/Printer_Pure"
+ Isabelle_Meta_Model.Printer_Pure
begin
context Print
diff --git a/Citadelle/src/compiler_generic/ROOT b/Citadelle/src/compiler_generic/ROOT
index 8dd9c505ced..aef7913c131 100644
--- a/Citadelle/src/compiler_generic/ROOT
+++ b/Citadelle/src/compiler_generic/ROOT
@@ -41,20 +41,6 @@
chapter AFP
-session Meta_Isabelle (AFP) = "HOL-Library" +
- description {* Meta_Isabelle *}
- options [timeout = 600, document = pdf, document_output = document_generated]
- theories [document = false]
- "isabelle_home/src/HOL/ex/Isabelle_Cartouche_Examples"
- "isabelle_home/src/Tools/Code/Isabelle_code_runtime"
- theories
- "meta_isabelle/Parser_Pure"
- "meta_isabelle/Meta_Isabelle"
- "meta_isabelle/Printer_Isabelle"
- document_files
- "root.bib"
- "root.tex"
-
session Isabelle_Meta_Model (AFP) = "HOL-Library" +
description {* Isabelle_Meta_Model containing a Toy Example *}
options [timeout = 600, document = pdf, document_output = document_generated]
@@ -83,23 +69,3 @@ session Isabelle_Meta_Model (AFP) = "HOL-Library" +
document_files
"root.bib"
"root.tex"
-
-(*
-session Toy_All = "HOL-Library" +
- description {* Toy_All *}
- options [timeout = 600, document = pdf, document_output = document_generated]
- theories [document = false]
- "isabelle_home/src/HOL/ex/Isabelle_Cartouche_Examples"
- "isabelle_home/src/Tools/Code/Isabelle_code_runtime"
- "isabelle_home/src/Pure/Isar/Isabelle_typedecl"
- theories
- "toy_example/embedding/Generator_static"
- (* "toy_example/embedding/Generator_dynamic_sequential" (* is imported by the following examples *) *)
- "toy_example/generator/Design_deep"
- "toy_example/generator/Design_shallow"
- "toy_example/document_generated/Design_generated_generated"
- "document/Rail"
- document_files
- "root.bib"
- "root.tex"
-*)
diff --git a/Citadelle/src/uml_ocl/UML_OCL.thy b/Citadelle/src/uml_ocl/UML_OCL.thy
index 8449b51bcf3..6bb69dc2f93 100644
--- a/Citadelle/src/uml_ocl/UML_OCL.thy
+++ b/Citadelle/src/uml_ocl/UML_OCL.thy
@@ -44,7 +44,7 @@
******************************************************************************)
theory UML_OCL
-imports "../uml_main/UML_Main"
+imports OCL.UML_Main
"../../examples/archive/Monads" (* NOTE: perform lazily the extraction of generation_syntax
so that dependencies can alternate among theories *)
"../compiler/Static"
--
GitLab