embedded latex has 0 length -- imitating \<^raw> before aa1fe1103ab8;
authorwenzelm
Sun Nov 27 13:13:26 2016 +0100 (2016-11-27)
changeset 6452601920e390645
parent 64525 9c3da2276e19
child 64527 49708cffb98d
embedded latex has 0 length -- imitating \<^raw> before aa1fe1103ab8;
src/Pure/Thy/latex.ML
     1.1 --- a/src/Pure/Thy/latex.ML	Fri Nov 25 14:10:33 2016 +0100
     1.2 +++ b/src/Pure/Thy/latex.ML	Sun Nov 27 13:13:26 2016 +0100
     1.3 @@ -106,21 +106,30 @@
     1.4    | Symbol.Malformed s => error (Symbol.malformed_msg s)
     1.5    | Symbol.EOF => error "Bad EOF symbol");
     1.6  
     1.7 +val scan_latex_length =
     1.8 +  Scan.many1 (fn (s, _) => Symbol.not_eof s andalso not (is_latex_control s))
     1.9 +    >> (Symbol.length o map Symbol_Pos.symbol) ||
    1.10 +  Scan.one (is_latex_control o Symbol_Pos.symbol) --
    1.11 +    Scan.option (Scan.permissive Symbol_Pos.scan_cartouche "") >> K 0;
    1.12 +
    1.13  fun scan_latex known =
    1.14    Scan.one (is_latex_control o Symbol_Pos.symbol) |--
    1.15      Symbol_Pos.scan_cartouche_content "Embedded LaTeX: " >> (implode o map Symbol_Pos.symbol) ||
    1.16    Scan.one (Symbol.not_eof o Symbol_Pos.symbol) >> (output_known_sym known o Symbol_Pos.symbol);
    1.17  
    1.18 -fun read_latex known syms =
    1.19 -  (case Scan.read Symbol_Pos.stopper (Scan.repeat (scan_latex known))
    1.20 -      (map (rpair Position.none) syms) of
    1.21 -    SOME ss => implode ss
    1.22 -  | NONE => error ("Malformed embedded LaTeX: " ^ quote (Symbol.beginning 10 syms)));
    1.23 +fun read scan syms =
    1.24 +  Scan.read Symbol_Pos.stopper (Scan.repeat scan) (map (rpair Position.none) syms);
    1.25  
    1.26  in
    1.27  
    1.28 +fun length_symbols syms =
    1.29 +  fold Integer.add (these (read scan_latex_length syms)) 0;
    1.30 +
    1.31  fun output_known_symbols known syms =
    1.32 -  if exists is_latex_control syms then read_latex known syms
    1.33 +  if exists is_latex_control syms then
    1.34 +    (case read (scan_latex known) syms of
    1.35 +      SOME ss => implode ss
    1.36 +    | NONE => error ("Malformed embedded LaTeX: " ^ quote (Symbol.beginning 10 syms)))
    1.37    else implode (map (output_known_sym known) syms);
    1.38  
    1.39  val output_symbols = output_known_symbols (K true, K true);
    1.40 @@ -201,7 +210,7 @@
    1.41  
    1.42  fun latex_output str =
    1.43    let val syms = Symbol.explode str
    1.44 -  in (output_symbols syms, Symbol.length syms) end;
    1.45 +  in (output_symbols syms, length_symbols syms) end;
    1.46  
    1.47  fun latex_markup (s, _) =
    1.48    if s = Markup.commandN orelse s = Markup.keyword1N orelse s = Markup.keyword3N