Avoid Parse_Spec.xthms1 and make theorem names clickable
authorJoachim Breitner <mail@joachim-breitner.de>
Fri, 19 Dec 2014 10:14:07 +0000 (11:14 +0100)
committerJoachim Breitner <mail@joachim-breitner.de>
Fri, 19 Dec 2014 10:14:07 +0000 (11:14 +0100)
(on a best effor basis. Theorem names with selectors are broken;
probably because the PThm constructor already has lost that information
when storing a theorem as a string.)

README.md
where_to_move.ML

index b1d6961..1ede9e5 100644 (file)
--- a/README.md
+++ b/README.md
@@ -128,8 +128,10 @@ Bugs and shortcomings
 
 These are the ones that I know about. If you have more, feel free to open an issue. 
 
- * The output does not use proper markup, i.e. you cannot click on the theorem
-   names and theory names, which would make this even more useful.
+ * In the output of `theorems_used_by`, if a theorem is actually a list of
+   them, and one is used, it prints the selector as part of the name
+   (`HOL.simp_thms_7`), which breaks the hyperlinking.
+ * Theory names are not clickable yet.
  * Definitions should be treated specially. Naturally, most `foo_def` lemmas can be moved to
    `HOL` (they are (derived from) axioms, after all), but I usually do not want to
    move definitions.
index 77cd0fd..69ba23d 100644 (file)
@@ -10,8 +10,8 @@ sig
   val theories_used_by_thm : theory -> thm -> theory list
   val theories_used_by_thms : theory -> thm list -> theory list
 
-  val theorems_used_by_cmd : (Facts.ref * Args.src list) list -> Toplevel.transition -> Toplevel.transition
-  val where_to_move_cmd : (Facts.ref * Args.src list) list option -> Toplevel.transition -> Toplevel.transition
+  val theorems_used_by_cmd : (string * Position.T) -> Toplevel.transition -> Toplevel.transition
+  val where_to_move_cmd : (string * Position.T) list option -> Toplevel.transition -> Toplevel.transition
 end
 
 structure Where_To_Move : WHERE_TO_MOVE =
@@ -19,7 +19,7 @@ struct
 
 fun thms_used_by_thm thm =
   let
-  fun  used_by_proof_body (PBody {thms, ...}) = thms |> map #2 |> map go |> List.concat
+  fun  used_by_proof_body (PBody {thms, ...}) = thms |> map #2 |> maps go
   and go ("", _, pbodyf) = pbodyf |> Future.join |> used_by_proof_body
     | go (s, _, _) = [s]
   in thm |> Thm.proof_body_of |> Proofterm.strip_thm |> used_by_proof_body
@@ -34,7 +34,7 @@ fun theories_used_by_thm thy thm =
           |> map (Context.this_theory thy);
 
 fun theories_used_by_thms thy thms =
-      thms |> map thms_used_by_thm  |> List.concat
+      thms |> maps thms_used_by_thm
            |> map (hd o Long_Name.explode) 
            |> nub 
            |> map (Context.this_theory thy);
@@ -51,28 +51,18 @@ fun better_theory thys this_thy =
   |> find_first  (ok_for thys);
 
 
-fun theorems_used_by_cmd args = Toplevel.keep (fn state => 
-    args |> Attrib.eval_thms (Toplevel.context_of state)
-         |> map thms_used_by_thm
-         |> map (Pretty.commas o map Pretty.str)
-         |> map (Pretty.writeln o Pretty.paragraph)
-         |> K ()
+fun theorems_used_by_cmd arg = Toplevel.keep (fn state =>
+    let val ctxt = Toplevel.context_of state
+        val thy = Toplevel.theory_of state
+        val (_, thms) =  Facts.retrieve (Context.Proof ctxt) (Global_Theory.facts_of thy) arg
+    in thms |> maps thms_used_by_thm
+            |> map (Pretty.mark_str o Proof_Context.markup_extern_fact ctxt)
+            |> Pretty.commas
+            |> Pretty.paragraph
+            |> Pretty.writeln
+    end
     );
 
-(* singleton variant of eval_thms *)
-fun eval_thm context arg = hd (Attrib.eval_thms context [arg])
-
-(* from find_theormes.ML *)
-fun pretty_ref _ thmref =
-  let
-    val (name, sel) =
-      (case thmref of
-        Facts.Named ((name, _), sel) => (name, sel)
-      | Facts.Fact _ => raise Fail "Illegal literal fact");
-  in Pretty.block
-  (*     [Pretty.mark(#1 (Proof_Context.markup_extern_fact ctxt name)) (Pretty.str name), *)
-    [Pretty.str name, Pretty.str (Facts.string_of_selection sel)]
-  end;
 
 fun facts_of_theory thy =
   let val prev_thys = (Theory.parents_of thy) 
@@ -82,21 +72,23 @@ fun facts_of_theory thy =
 
 fun where_to_move_cmd args_o =
   Toplevel.keep ( fn state =>
-    let val named_thms = case args_o of
-            SOME args => args |> map (fn arg =>
-              (Pretty.string_of (pretty_ref (Toplevel.context_of state) (#1 arg)),
-              [ eval_thm (Toplevel.context_of state) arg] ))
-            | NONE => facts_of_theory (Toplevel.theory_of state)
+    let val ctxt = Toplevel.context_of state
+        val this_thy = Toplevel.theory_of state
+        val named_thms = case args_o of
+            SOME args => args |> map (Facts.retrieve (Context.Proof ctxt) (Global_Theory.facts_of this_thy))
+            | NONE => facts_of_theory this_thy
     in named_thms |> map (fn (name, thms) =>
-    let  val thy = Toplevel.theory_of state
-    in case better_theory (theories_used_by_thms thy thms) thy of
-        SOME thy => Pretty.writeln (Pretty.paragraph
-         [ Pretty.str "Theorem ", Pretty.str name,
-           Pretty.str " could be moved to theory ",
-           Pretty.quote (Pretty.str (Context.theory_name thy)), Pretty.str "."
-         ])
-      | NONE     => Pretty.writeln (Pretty.paragraph [Pretty.str "Theorem ", Pretty.str name, Pretty.str" is fine where it is."])
-    end
+      let val pretty_name = Pretty.mark_str (Proof_Context.markup_extern_fact ctxt name)
+      in case better_theory (theories_used_by_thms this_thy thms) this_thy of
+          SOME thy =>
+           [ Pretty.str "Theorem ", pretty_name,
+             Pretty.str " could be moved to theory ",
+             Pretty.quote (Pretty.str (Context.theory_name thy)), Pretty.str "."
+           ]
+        | NONE =>
+           [ Pretty.str "Theorem ", pretty_name,
+             Pretty.str" is fine where it is."]
+      end |> Pretty.paragraph |> Pretty.writeln
     ) |> K ()
    end
    );
@@ -104,10 +96,10 @@ fun where_to_move_cmd args_o =
 
 val _ = Outer_Syntax.improper_command @{command_spec "theorems_used_by"} 
     "prints all theorems used by the given theorem"
-    (Parse_Spec.xthms1 >> theorems_used_by_cmd);
+    (Parse.position Parse.xname >> theorems_used_by_cmd);
 
 val _ = Outer_Syntax.improper_command @{command_spec "where_to_move"}
     "suggests a new location for the given theorem or, of none is given, all theorems in the current theory"
-    (Scan.option Parse_Spec.xthms1 >> where_to_move_cmd);
+    (Scan.option (Scan.repeat1 (Parse.position Parse.xname)) >> where_to_move_cmd);
 
 end