tuned signature;
authorwenzelm
Mon Mar 10 15:30:29 2014 +0100 (2014-03-10)
changeset 56028422024102d9d
parent 56027 25889f5c39a8
child 56029 8bedca4bd5a3
tuned signature;
src/Pure/Isar/args.ML
src/Pure/Thy/thy_output.ML
     1.1 --- a/src/Pure/Isar/args.ML	Mon Mar 10 15:20:41 2014 +0100
     1.2 +++ b/src/Pure/Isar/args.ML	Mon Mar 10 15:30:29 2014 +0100
     1.3 @@ -10,6 +10,7 @@
     1.4    type src
     1.5    val src: (string * Token.T list) * Position.T -> src
     1.6    val dest_src: src -> (string * Token.T list) * Position.T
     1.7 +  val unparse_src: src -> string list
     1.8    val pretty_src: (string -> Pretty.T) -> Proof.context -> src -> Pretty.T
     1.9    val map_name: (string -> string) -> src -> src
    1.10    val transform_values: morphism -> src -> src
    1.11 @@ -79,6 +80,8 @@
    1.12  val src = Src;
    1.13  fun dest_src (Src src) = src;
    1.14  
    1.15 +fun unparse_src (Src ((_, toks), _)) = map Token.unparse toks;
    1.16 +
    1.17  fun pretty_src pretty_name ctxt src =
    1.18    let
    1.19      val prt_thm = Pretty.backquote o Display.pretty_thm ctxt;
     2.1 --- a/src/Pure/Thy/thy_output.ML	Mon Mar 10 15:20:41 2014 +0100
     2.2 +++ b/src/Pure/Thy/thy_output.ML	Mon Mar 10 15:30:29 2014 +0100
     2.3 @@ -529,7 +529,7 @@
     2.4  
     2.5  (* default output *)
     2.6  
     2.7 -val str_of_source = space_implode " " o map Token.unparse o #2 o #1 o Args.dest_src;
     2.8 +val str_of_source = space_implode " " o Args.unparse_src;
     2.9  
    2.10  fun maybe_pretty_source pretty ctxt src xs =
    2.11    map (pretty ctxt) xs  (*always pretty in order to exhibit errors!*)