merged
authorwenzelm
Wed May 16 15:52:15 2018 +0200 (12 months ago)
changeset 68195607957640057
parent 68191 4ac04fe61e98
parent 68194 796f2585c7ee
child 68196 756434c77d21
merged
     1.1 --- a/src/Pure/Thy/thy_output.ML	Tue May 15 21:19:22 2018 +0200
     1.2 +++ b/src/Pure/Thy/thy_output.ML	Wed May 16 15:52:15 2018 +0200
     1.3 @@ -117,13 +117,14 @@
     1.4        |> maps output_symbols_antiq
     1.5    | (SOME comment, _) => output_comment ctxt (comment, syms));
     1.6  
     1.7 -in
     1.8 -
     1.9  fun output_body ctxt antiq bg en syms =
    1.10    Comment.read_body syms
    1.11    |> maps (output_comment_symbols ctxt {antiq = antiq})
    1.12 -  |> Latex.enclose_body bg en
    1.13 -and output_token ctxt tok =
    1.14 +  |> Latex.enclose_body bg en;
    1.15 +
    1.16 +in
    1.17 +
    1.18 +fun output_token ctxt tok =
    1.19    let
    1.20      fun output antiq bg en =
    1.21        output_body ctxt antiq bg en (Input.source_explode (Token.input_of tok));
     2.1 --- a/src/Pure/context.ML	Tue May 15 21:19:22 2018 +0200
     2.2 +++ b/src/Pure/context.ML	Wed May 16 15:52:15 2018 +0200
     2.3 @@ -177,7 +177,7 @@
     2.4  fun display_names thy =
     2.5    let
     2.6      val name = display_name (theory_id thy);
     2.7 -    val ancestor_names = map theory_name (ancestors_of thy);
     2.8 +    val ancestor_names = map theory_long_name (ancestors_of thy);
     2.9    in rev (name :: ancestor_names) end;
    2.10  
    2.11  val pretty_thy = Pretty.str_list "{" "}" o display_names;
    2.12 @@ -359,7 +359,7 @@
    2.13  
    2.14  val update_thy = change_thy false;
    2.15  val extend_thy = update_thy I;
    2.16 -val finish_thy = change_thy true I;
    2.17 +val finish_thy = change_thy true I #> tap extend_thy;
    2.18  
    2.19  end;
    2.20  
    2.21 @@ -399,7 +399,7 @@
    2.22  
    2.23        val history = make_history name 0;
    2.24        val ancestry = make_ancestry parents ancestors;
    2.25 -    in create_thy ids history ancestry (data_of thy0) end;
    2.26 +    in create_thy ids history ancestry (data_of thy0) |> tap finish_thy end;
    2.27  
    2.28  end;
    2.29