consolidated terminology

--- a/src/Pure/Isar/outer_syntax.ML	Sat Oct 10 18:43:07 2020 +0000
+++ b/src/Pure/Isar/outer_syntax.ML	Sat Oct 10 18:43:09 2020 +0000
@@ -156,7 +156,7 @@
       Parse.opt_target -- parse_local
         >> (fn (target, f) => Toplevel.local_theory restricted target f) ||
       (if is_some restricted then Scan.fail
-       else parse_global >> Toplevel.begin_local_theory true)));
+       else parse_global >> Toplevel.begin_main_target true)));
 
 fun local_theory_command trans command_keyword comment parse =
   raw_command command_keyword comment

--- a/src/Pure/Isar/toplevel.ML	Sat Oct 10 18:43:07 2020 +0000
+++ b/src/Pure/Isar/toplevel.ML	Sat Oct 10 18:43:09 2020 +0000
@@ -52,10 +52,10 @@
   val generic_theory: (generic_theory -> generic_theory) -> transition -> transition
   val theory': (bool -> theory -> theory) -> transition -> transition
   val theory: (theory -> theory) -> transition -> transition
-  val begin_local_theory: bool -> (theory -> local_theory) -> transition -> transition
-  val end_local_theory: transition -> transition
-  val open_target: (generic_theory -> local_theory) -> transition -> transition
-  val close_target: transition -> transition
+  val begin_main_target: bool -> (theory -> local_theory) -> transition -> transition
+  val end_main_target: transition -> transition
+  val begin_nested_target: (generic_theory -> local_theory) -> transition -> transition
+  val end_nested_target: transition -> transition
   val local_theory': (bool * Position.T) option -> (xstring * Position.T) option ->
     (bool -> local_theory -> local_theory) -> transition -> transition
   val local_theory: (bool * Position.T) option -> (xstring * Position.T) option ->
@@ -432,7 +432,7 @@
 
 fun theory f = theory' (K f);
 
-fun begin_local_theory begin f = transaction (fn _ =>
+fun begin_main_target begin f = transaction (fn _ =>
   (fn Theory (Context.Theory thy) =>
         let
           val lthy = f thy;
@@ -444,17 +444,17 @@
         in (Theory gthy, lthy) end
     | _ => raise UNDEF));
 
-val end_local_theory = transaction (fn _ =>
+val end_main_target = transaction (fn _ =>
   (fn Theory (Context.Proof lthy) => (Theory (Context.Theory (Named_Target.exit lthy)), lthy)
     | _ => raise UNDEF));
 
-fun open_target f = transaction0 (fn _ =>
+fun begin_nested_target f = transaction0 (fn _ =>
   (fn Theory gthy =>
         let val lthy = f gthy
         in Theory (Context.Proof lthy) end
     | _ => raise UNDEF));
 
-val close_target = transaction (fn _ =>
+val end_nested_target = transaction (fn _ =>
   (fn Theory (Context.Proof lthy) =>
         (case try Local_Theory.close_target lthy of
           SOME ctxt' =>

--- a/src/Pure/Pure.thy	Sat Oct 10 18:43:07 2020 +0000
+++ b/src/Pure/Pure.thy	Sat Oct 10 18:43:09 2020 +0000
@@ -626,15 +626,15 @@
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>context\<close> "begin local theory context"
-    ((Parse.name_position >> (Toplevel.begin_local_theory true o Named_Target.begin) ||
+    ((Parse.name_position >> (Toplevel.begin_main_target true o Named_Target.begin) ||
       Scan.optional Parse_Spec.includes [] -- Scan.repeat Parse_Spec.context_element
-        >> (fn (incls, elems) => Toplevel.open_target (#2 o Bundle.context_cmd incls elems)))
+        >> (fn (incls, elems) => Toplevel.begin_nested_target (#2 o Bundle.context_cmd incls elems)))
       --| Parse.begin);
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>end\<close> "end context"
     (Scan.succeed
-      (Toplevel.exit o Toplevel.end_local_theory o Toplevel.close_target o
+      (Toplevel.exit o Toplevel.end_main_target o Toplevel.end_nested_target o
         Toplevel.end_proof (K Proof.end_notepad)));
 
 in end\<close>
@@ -655,14 +655,14 @@
     (Parse.binding --
       Scan.optional (\<^keyword>\<open>=\<close> |-- Parse.!!! locale_val) (([], []), []) -- Parse.opt_begin
       >> (fn ((name, (expr, elems)), begin) =>
-          Toplevel.begin_local_theory begin
+          Toplevel.begin_main_target begin
             (Expression.add_locale_cmd name Binding.empty expr elems #> snd)));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>experiment\<close> "open private specification context"
     (Scan.repeat Parse_Spec.context_element --| Parse.begin
       >> (fn elems =>
-          Toplevel.begin_local_theory true (Experiment.experiment_cmd elems #> snd)));
+          Toplevel.begin_main_target true (Experiment.experiment_cmd elems #> snd)));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>interpret\<close>
@@ -714,7 +714,7 @@
   Outer_Syntax.command \<^command_keyword>\<open>class\<close> "define type class"
    (Parse.binding -- Scan.optional (\<^keyword>\<open>=\<close> |-- class_val) ([], []) -- Parse.opt_begin
     >> (fn ((name, (supclasses, elems)), begin) =>
-        Toplevel.begin_local_theory begin
+        Toplevel.begin_main_target begin
           (Class_Declaration.class_cmd name supclasses elems #> snd)));
 
 val _ =
@@ -724,7 +724,7 @@
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>instantiation\<close> "instantiate and prove type arity"
    (Parse.multi_arity --| Parse.begin
-     >> (fn arities => Toplevel.begin_local_theory true (Class.instantiation_cmd arities)));
+     >> (fn arities => Toplevel.begin_main_target true (Class.instantiation_cmd arities)));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>instance\<close> "prove type arity or subclass relation"
@@ -746,7 +746,7 @@
    (Scan.repeat1 (Parse.name --| (\<^keyword>\<open>==\<close> || \<^keyword>\<open>\<equiv>\<close>) -- Parse.term --
       Scan.optional (\<^keyword>\<open>(\<close> |-- (\<^keyword>\<open>unchecked\<close> >> K false) --| \<^keyword>\<open>)\<close>) true
       >> Scan.triple1) --| Parse.begin
-   >> (fn operations => Toplevel.begin_local_theory true (Overloading.overloading_cmd operations)));
+   >> (fn operations => Toplevel.begin_main_target true (Overloading.overloading_cmd operations)));
 
 in end\<close>