tuned signature;
authorwenzelm
Mon Nov 26 11:59:56 2012 +0100 (2012-11-26 ago)
changeset 502124fb06c22c5ec
parent 50211 2a3d6d760629
child 50213 7b73c0509835
tuned signature;
src/HOL/Tools/Nitpick/nitpick.ML
src/Pure/PIDE/sendback.ML
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Mon Nov 26 11:42:16 2012 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Mon Nov 26 11:59:56 2012 +0100
     1.3 @@ -470,7 +470,7 @@
     1.4                pprint_nt (fn () => Pretty.blk (0,
     1.5                    pstrs "Hint: To check that the induction hypothesis is \
     1.6                          \general enough, try this command: " @
     1.7 -                  [Pretty.mark (Sendback.make_markup ()) (Pretty.blk (0,
     1.8 +                  [Pretty.mark (Sendback.make_markup {implicit = false}) (Pretty.blk (0,
     1.9                         pstrs ("nitpick [non_std, show_all]")))] @ pstrs "."))
    1.10              else
    1.11                ()
     2.1 --- a/src/Pure/PIDE/sendback.ML	Mon Nov 26 11:42:16 2012 +0100
     2.2 +++ b/src/Pure/PIDE/sendback.ML	Mon Nov 26 11:59:56 2012 +0100
     2.3 @@ -7,25 +7,26 @@
     2.4  
     2.5  signature SENDBACK =
     2.6  sig
     2.7 -  val make_markup: unit -> Markup.T
     2.8 +  val make_markup: {implicit: bool} -> Markup.T
     2.9 +  val markup_implicit: string -> string
    2.10    val markup: string -> string
    2.11 -  val markup_implicit: string -> string
    2.12  end;
    2.13  
    2.14  structure Sendback: SENDBACK =
    2.15  struct
    2.16  
    2.17 -fun make_markup () =
    2.18 -  let
    2.19 -    val props =
    2.20 -      (case Position.get_id (Position.thread_data ()) of
    2.21 -        SOME id => [(Markup.idN, id)]
    2.22 -      | NONE => []);
    2.23 -  in Markup.properties props Markup.sendback end;
    2.24 +fun make_markup {implicit} =
    2.25 +  if implicit then Markup.sendback
    2.26 +  else
    2.27 +    let
    2.28 +      val props =
    2.29 +        (case Position.get_id (Position.thread_data ()) of
    2.30 +          SOME id => [(Markup.idN, id)]
    2.31 +        | NONE => []);
    2.32 +    in Markup.properties props Markup.sendback end;
    2.33  
    2.34 -fun markup s = Markup.markup (make_markup ()) s;
    2.35 -
    2.36 -fun markup_implicit s = Markup.markup Markup.sendback s;
    2.37 +fun markup_implicit s = Markup.markup (make_markup {implicit = true}) s;
    2.38 +fun markup s = Markup.markup (make_markup {implicit = false}) s;
    2.39  
    2.40  end;
    2.41