#! /usr/bin/awk -f

function emit_buffer() {
  print indent buffer;
  buffer = "";
}

BEGIN {
  buffer = "";
  indent = "";
}

/^ *#line [0-9]/ {
  indent=buffer;
  buffer="";
}

/^  */ {
  if (length(buffer) > 0) gsub("^ *", "");
}

/\\begin_inset Newline newline$/ {
  if (NR > 1) emit_buffer();
}

/^ *\\backslash/ {
  buffer = buffer "\\";
  $0 = "";
}

/\\/ {
  gsub("\\\\.*$", "");
}

{
  buffer = buffer $0;
}

END {
  if (length(buffer) > 0) emit_buffer();
}