option document_positions;
authorwenzelm
Tue Dec 12 17:46:22 2017 +0100 (17 months ago)
changeset 671919ab34bb83a84
parent 67190 58ab7ddbdb04
child 67192 26f548370e8d
option document_positions;
NEWS
etc/options
src/Pure/Thy/thy_output.ML
     1.1 --- a/NEWS	Tue Dec 12 17:47:23 2017 +0100
     1.2 +++ b/NEWS	Tue Dec 12 17:46:22 2017 +0100
     1.3 @@ -87,8 +87,12 @@
     1.4  more accurately: only terminal proof steps ('by' etc.) are skipped.
     1.5  
     1.6  * Command-line tool "isabelle document" has been re-implemented in
     1.7 -Isabelle/Scala, with simplified arguments and explicit errors from the
     1.8 -latex process. Minor INCOMPATIBILITY.
     1.9 +Isabelle/Scala, with simplified arguments. Minor INCOMPATIBILITY.
    1.10 +
    1.11 +* Original source positions are inlined into generated tex files: this
    1.12 +improves error messages by "isabelle document", but may sometimes
    1.13 +confuse LaTeX. Rare INCOMPATIBILITY, set option
    1.14 +"document_positions=false" to avoid this.
    1.15  
    1.16  
    1.17  *** HOL ***
     2.1 --- a/etc/options	Tue Dec 12 17:47:23 2017 +0100
     2.2 +++ b/etc/options	Tue Dec 12 17:46:22 2017 +0100
     2.3 @@ -13,6 +13,8 @@
     2.4    -- "alternative document variants (separated by colons)"
     2.5  option document_tags : string = ""
     2.6    -- "default command tags (separated by commas)"
     2.7 +option document_positions : bool = true
     2.8 +  -- "inline original source positions into generated tex files"
     2.9  
    2.10  option thy_output_display : bool = false
    2.11    -- "indicate output as multi-line display-style material"
     3.1 --- a/src/Pure/Thy/thy_output.ML	Tue Dec 12 17:47:23 2017 +0100
     3.2 +++ b/src/Pure/Thy/thy_output.ML	Tue Dec 12 17:46:22 2017 +0100
     3.3 @@ -262,18 +262,18 @@
     3.4  val blank_token = basic_token Token.is_blank;
     3.5  val newline_token = basic_token Token.is_newline;
     3.6  
     3.7 -fun present_token state tok =
     3.8 +fun present_token {positions} state tok =
     3.9    (case tok of
    3.10      No_Token => ""
    3.11 -  | Basic_Token tok => Latex.output_token tok |> Latex.line_output (Token.pos_of tok)
    3.12 +  | Basic_Token tok => Latex.output_token tok |> positions ? Latex.line_output (Token.pos_of tok)
    3.13    | Markup_Token (cmd, source) =>
    3.14        "%\n\\isamarkup" ^ cmd ^ "{" ^
    3.15 -        output_text state {markdown = false, positions = true} source ^ "%\n}\n"
    3.16 +        output_text state {markdown = false, positions = positions} source ^ "%\n}\n"
    3.17    | Markup_Env_Token (cmd, source) =>
    3.18        Latex.environment ("isamarkup" ^ cmd)
    3.19 -        (output_text state {markdown = true, positions = true} source)
    3.20 +        (output_text state {markdown = true, positions = positions} source)
    3.21    | Raw_Token source =>
    3.22 -      "%\n" ^ output_text state {markdown = true, positions = true} source ^ "\n");
    3.23 +      "%\n" ^ output_text state {markdown = true, positions = positions} source ^ "\n");
    3.24  
    3.25  
    3.26  (* command spans *)
    3.27 @@ -316,11 +316,11 @@
    3.28  
    3.29  in
    3.30  
    3.31 -fun present_span keywords document_tags span state state'
    3.32 +fun present_span positions keywords document_tags span state state'
    3.33      (tag_stack, active_tag, newline, buffer, present_cont) =
    3.34    let
    3.35      val present = fold (fn (tok, (flag, 0)) =>
    3.36 -        Buffer.add (present_token state' tok)
    3.37 +        Buffer.add (present_token positions state' tok)
    3.38          #> Buffer.add flag
    3.39        | _ => I);
    3.40  
    3.41 @@ -413,6 +413,7 @@
    3.42  
    3.43  fun present_thy thy command_results toks =
    3.44    let
    3.45 +    val positions = Options.default_bool \<^system_option>\<open>document_positions\<close>;
    3.46      val keywords = Thy_Header.get_keywords thy;
    3.47  
    3.48  
    3.49 @@ -492,7 +493,8 @@
    3.50      val document_tags = space_explode "," (Options.default_string \<^system_option>\<open>document_tags\<close>);
    3.51  
    3.52      fun present_command tr span st st' =
    3.53 -      Toplevel.setmp_thread_position tr (present_span keywords document_tags span st st');
    3.54 +      Toplevel.setmp_thread_position tr
    3.55 +        (present_span {positions = positions} keywords document_tags span st st');
    3.56  
    3.57      fun present _ [] = I
    3.58        | present st (((tr, st'), span) :: rest) = present_command tr span st st' #> present st' rest;