theory Latex imports
 Main
keywords
 "export_snippets" :: thy_decl
begin  

text \<open>

Usage: invoke @{command export_snippets} in theories you want
to generate snippets of. They will end up in the document output;
you might need sth like @{verbatim "-e *:document/snippets.tex"} on
@{verbatim "isabelle build"}.

Otherwise, find the output under @{verbatim "isabelle-export:"}
in the file browser panel.
\<close>

ML \<open>

fun export_snippet searchterm lthy = Thy_Info.add_presentation (fn {options, segments, ...} => fn thy => 
  let
    val keywords = Thy_Header.get_keywords thy;
    val thy_name = Context.theory_base_name thy;

    val segments_grouped = fold
      (fn s => fn a::acc => if Toplevel.is_proof (#prev_state s)
        then (a @ [s]) :: acc else [s] :: a :: acc) (tl segments) [[hd segments]]
    |> rev
    |> filter (fn segments => not (Toplevel.is_ignored (#command (hd segments))))

    val segments_filtered = if searchterm = "" then segments_grouped else
      filter (fn segments => Toplevel.name_of (#command (hd segments)) = searchterm) segments_grouped;

    val segment_names = segments_filtered
      |> map (fn segments =>
        let
          val {span, command,...} = hd segments
          val nonblank = filter (not o Token.is_space) (Command_Span.content span)
          val name = case nonblank of
              _ :: name :: _ => Token.content_of name
            | _ => ""
          val symbols = name
            |> Symbol.explode
            |> map (fn sym => 
                 if Symbol.is_ascii_letter sym orelse Symbol.is_ascii_digit sym 
                 then sym else if Symbol.is_printable sym then "-" else "")
          val looks_like_name = not (exists (Symbol.is_blank) symbols) andalso length symbols <> 0;
          val command_name = Toplevel.name_of command
        in (not looks_like_name, command_name ^ ":" ^ (if looks_like_name then String.concat symbols else "")) end);

    val markup = segments_filtered
      |> map (fn segments =>
           SOME (YXML.parse_body (XML.content_of (Scan.catch (Document_Output.present_thy options keywords thy_name) segments)))
           handle Fail _ => NONE)

    fun render_macro_lines snippet_name stack n kind attrs trees = 
      case AList.lookup (op =) attrs "name" of
      SOME name =>
        let 
          val macro = "isa" ^ kind ^ name ^ "\n";
          val (n', content) = fold (fn t => fn (n, ts) =>
             let val (n', t) = render_lines snippet_name (macro :: stack) n t
             in (n', t::ts) end) trees (n,[])
        in if name = "invisible" then (n,"") else (n', "\\" ^ macro 
           ^ String.concat (rev content)
           ^ "\\end" ^ macro) 
        end
      | NONE => error "terru misunderstood the YXML"
    and render_lines snippet_name stack n (XML.Text str) = 
         let
           val chunks = Metis_Useful.split "\\isanewline\n" str;
           val n' = length chunks;
           val breaker = fn n => fold (fn m => fn acc => "%\n\\end" ^ m ^ acc ^ "\\" ^ m) 
                  stack ("\\isanewline}%\n\\SNIP{" ^ snippet_name ^ "-" ^ string_of_int n ^ "}{%\n");
           val broken = chunks
             |> map_index (fn (i, a) => if i = length chunks - 1 then a else a ^ breaker (1+i+n));
         in (n+n'-1, String.concat broken) end
      | render_lines snippet_name stack n (XML.Elem ((name, attrs), trees)) =  case name of
           "latex_delim" => render_macro_lines snippet_name stack n "delim" attrs trees
         | "latex_tag" => render_macro_lines snippet_name stack n "tag" attrs trees
         | tag =>
            let
              val _ = warning ("unknown markup tag " ^ tag);
              val (n', content) = fold (fn t => fn (n, ts) =>
                let val (m, t) = render_lines snippet_name stack n t
                in (m, t::ts) end) trees (n,[]);
            in (n', String.concat (rev content)) end
    val snippets = markup
      |> Metis_Useful.zip segment_names (* why is this only in metis ?? *)
      |> map_filter (fn ((needs_hash, name), SOME texchunks) => 
          if length texchunks > 0 (* otherwise only header/footer, no content *)
          then let 
             val snippet_name = if needs_hash then let val hash = XML.content_of texchunks
               |> (SHA1.rep o SHA1.digest)
               |> Symbol.explode
               |> take 6
               |> String.concat
              in name ^ hash end else name
             val (_, latex) = fold (fn chunk => fn (n, lines) => 
                 let val (n', content) = render_lines snippet_name [] n chunk
                 in (n', content::lines) end) (( texchunks)) (0,[])
             val body = String.concat (rev latex)
               |> unprefix "%\n\\begin{isabellebody}%\n"
               |> unsuffix "%\n\\end{isabellebody}%\n"
            in SOME ("\\SNIP{" ^ snippet_name ^ "-0" ^ "}{%\n" ^ body ^ "}%\n") end
          else NONE 
        | (_, NONE) => NONE)
    val binding = \<^path_binding>\<open>snippets\<close>
      |> Path.map_binding (fn dir => Path.append dir (Path.basic ("snippets_"^thy_name^".tex")))
  in
    Export.export thy binding (map XML.Text (snippets))
  end
) lthy;

val _ =
  Outer_Syntax.local_theory \<^command_keyword>\<open>export_snippets\<close> "export LaTeX snippet"
    (Scan.optional Parse.string "" >> (fn name =>
       Local_Theory.background_theory (fn thy => (
         writeln (Export.message thy (Path.basic "snippets"));
         export_snippet name thy))));

\<close>

export_snippets

end