diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-06-12 17:12:51 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-06-12 17:27:53 +0200 |
| commit | ab53757a3bf57ced503023f3cf9dea5b5503dfea (patch) | |
| tree | 97241209c0348d72fda82fa33d67095f39d32da3 /printing | |
| parent | 79c42e22dd5106dcb85229ceec75331029ab5486 (diff) | |
[proof] Move bullets to their own module.
Bullets were placed inside the `Proof_global` module, I guess that due
to the global registration function. However, it has logically nothing
to do with the functionality of `Proof_global` and the current
placement may create some interference between the developers
reworking proof state handling and bullets.
We thus put the bullet functionality into its own, independent file.
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/ppvernac.ml | 6 | ||||
| -rw-r--r-- | printing/printer.ml | 2 |
2 files changed, 4 insertions, 4 deletions
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 781af4789..ca1499bc2 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -105,7 +105,7 @@ open Decl_kinds | SearchString (s,sc) -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc let pr_search a gopt b pr_p = - pr_opt (fun g -> Proof_global.pr_goal_selector g ++ str ":"++ spc()) gopt + pr_opt (fun g -> Proof_bullet.pr_goal_selector g ++ str ":"++ spc()) gopt ++ match a with | SearchHead c -> keyword "SearchHead" ++ spc() ++ pr_p c ++ pr_in_out_modules b @@ -490,7 +490,7 @@ open Decl_kinds | PrintVisibility s -> keyword "Print Visibility" ++ pr_opt str s | PrintAbout (qid,gopt) -> - pr_opt (fun g -> Proof_global.pr_goal_selector g ++ str ":"++ spc()) gopt + pr_opt (fun g -> Proof_bullet.pr_goal_selector g ++ str ":"++ spc()) gopt ++ keyword "About" ++ spc() ++ pr_smart_global qid | PrintImplicit qid -> keyword "Print Implicit" ++ spc() ++ pr_smart_global qid @@ -1130,7 +1130,7 @@ open Decl_kinds | None -> hov 2 (keyword "Check" ++ spc() ++ pr_lconstr c) in let pr_i = match io with None -> mt () - | Some i -> Proof_global.pr_goal_selector i ++ str ": " in + | Some i -> Proof_bullet.pr_goal_selector i ++ str ": " in return (pr_i ++ pr_mayeval r c) | VernacGlobalCheck c -> return (hov 2 (keyword "Type" ++ pr_constrarg c)) diff --git a/printing/printer.ml b/printing/printer.ml index 3c31dd96b..58cfc2b88 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -798,7 +798,7 @@ let pr_open_subgoals ?(proof=Proof_global.give_me_the_proof ()) () = | _ , _, _ -> let end_cmd = str "This subproof is complete, but there are some unfocused goals." ++ - (let s = Proof_global.Bullet.suggest p in + (let s = Proof_bullet.suggest p in if Pp.ismt s then s else fnl () ++ s) ++ fnl () in |