simplified / modernized hide commands: proper outer parsers and PIDE markup via check;

--- a/src/Pure/Isar/isar_cmd.ML	Sun Mar 09 17:07:45 2014 +0100
+++ b/src/Pure/Isar/isar_cmd.ML	Sun Mar 09 17:08:31 2014 +0100
@@ -21,10 +21,6 @@
     Symbol_Pos.source -> local_theory -> local_theory
   val simproc_setup: string * Position.T -> string list -> Symbol_Pos.source ->
     string list -> local_theory -> local_theory
-  val hide_class: bool -> xstring list -> theory -> theory
-  val hide_type: bool -> xstring list -> theory -> theory
-  val hide_const: bool -> xstring list -> theory -> theory
-  val hide_fact: bool -> xstring list -> theory -> theory
   val have: (Attrib.binding * (string * string list) list) list -> bool -> Proof.state -> Proof.state
   val hence: (Attrib.binding * (string * string list) list) list -> bool -> Proof.state -> Proof.state
   val show: (Attrib.binding * (string * string list) list) list -> bool -> Proof.state -> Proof.state
@@ -183,24 +179,6 @@
   |> Context.proof_map;
 
 
-(* hide names *)
-
-fun hide_names intern check hide fully xnames thy =
-  let
-    val names = map (intern thy) xnames;
-    val bads = filter_out (check thy) names;
-  in
-    if null bads then fold (hide fully) names thy
-    else error ("Attempt to hide undeclared item(s): " ^ commas_quote bads)
-  end;
-
-val hide_class = hide_names Sign.intern_class (can o Sign.certify_class) Sign.hide_class;
-val hide_type = hide_names Sign.intern_type Sign.declared_tyname Sign.hide_type;
-val hide_const = hide_names Sign.intern_const Sign.declared_const Sign.hide_const;
-val hide_fact =
-  hide_names Global_Theory.intern_fact Global_Theory.defined_fact Global_Theory.hide_fact;
-
-
 (* goals *)
 
 fun goal opt_chain goal stmt int =

--- a/src/Pure/Isar/isar_syn.ML	Sun Mar 09 17:07:45 2014 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Sun Mar 09 17:08:31 2014 +0100
@@ -231,17 +231,36 @@
           #2 oo Specification.theorems_cmd "" [(Attrib.empty_binding, flat facts)] fixes));
 
 
-(* name space entry path *)
+(* hide names *)
+
+local
+
+fun hide_names command_spec what hide parse prep =
+  Outer_Syntax.command command_spec ("hide " ^ what ^ " from name space")
+    ((Parse.opt_keyword "open" >> not) -- Scan.repeat1 parse >> (fn (fully, args) =>
+      (Toplevel.theory (fn thy =>
+        let val ctxt = Proof_Context.init_global thy
+        in fold (hide fully o prep ctxt) args thy end))));
+
+in
 
-fun hide_names spec hide what =
-  Outer_Syntax.command spec ("hide " ^ what ^ " from name space")
-    ((Parse.opt_keyword "open" >> not) -- Scan.repeat1 Parse.xname >>
-      (Toplevel.theory o uncurry hide));
+val _ =
+  hide_names @{command_spec "hide_class"} "classes" Sign.hide_class Parse.class
+    Proof_Context.read_class;
+
+val _ =
+  hide_names @{command_spec "hide_type"} "types" Sign.hide_type Parse.type_const
+    ((#1 o dest_Type) oo Proof_Context.read_type_name {proper = true, strict = false});
 
-val _ = hide_names @{command_spec "hide_class"} Isar_Cmd.hide_class "classes";
-val _ = hide_names @{command_spec "hide_type"} Isar_Cmd.hide_type "types";
-val _ = hide_names @{command_spec "hide_const"} Isar_Cmd.hide_const "constants";
-val _ = hide_names @{command_spec "hide_fact"} Isar_Cmd.hide_fact "facts";
+val _ =
+  hide_names @{command_spec "hide_const"} "constants" Sign.hide_const Parse.const
+    ((#1 o dest_Const) oo Proof_Context.read_const {proper = true, strict = false});
+
+val _ =
+  hide_names @{command_spec "hide_fact"} "facts" Global_Theory.hide_fact
+    (Parse.position Parse.xname) (Global_Theory.check_fact o Proof_Context.theory_of);
+
+end;
 
 
 (* use ML text *)